SMT-based automatic proof of ASM model refinement

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F16%3A10331960" target="_blank" >RIV/00216208:11320/16:10331960 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1007/978-3-319-41591-8_17" target="_blank" >http://dx.doi.org/10.1007/978-3-319-41591-8_17</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-319-41591-8_17" target="_blank" >10.1007/978-3-319-41591-8_17</a>

Jazyk výsledku

angličtina

Název v původním jazyce

SMT-based automatic proof of ASM model refinement

Popis výsledku v původním jazyce

Model refinement is a technique indispensable for modeling large and complex systems. Many formal specification methods share this concept which usually comes together with the definition of refinement correctness, i.e., the mathematical proof of a logical relation between an abstract model and its refined models. Model refinement is one of the main concepts which the Abstract State Machine (ASM) formal method is built on. Proofs of correct model refinement are usually performed manually, which reduces the usability of the ASM model refinement approach. An automatic support to assist the developer in proving refinement correctness along the chain of refinement steps could be of extreme importance to improve, in practice, the adoption of ASMs. In this paper, we present how the integration between the ASMs and Satisfiability Modulo Theories (SMT) can be used to automatically prove correctness of model refinement for the ASM method.

Název v anglickém jazyce

SMT-based automatic proof of ASM model refinement

Popis výsledku anglicky

Model refinement is a technique indispensable for modeling large and complex systems. Many formal specification methods share this concept which usually comes together with the definition of refinement correctness, i.e., the mathematical proof of a logical relation between an abstract model and its refined models. Model refinement is one of the main concepts which the Abstract State Machine (ASM) formal method is built on. Proofs of correct model refinement are usually performed manually, which reduces the usability of the ASM model refinement approach. An automatic support to assist the developer in proving refinement correctness along the chain of refinement steps could be of extreme importance to improve, in practice, the adoption of ASMs. In this paper, we present how the integration between the ASMs and Satisfiability Modulo Theories (SMT) can be used to automatically prove correctness of model refinement for the ASM method.

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

<a href="/cs/project/GA14-11384S" target="_blank" >GA14-11384S: Automatizovaná formální analýza a verifikace programů se složitými datovými a řídicími strukturami s předem neomezenou velikostí</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2016

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Software Engineering and Formal Methods: 14th International Conference, SEFM 2016, Held as Part of STAF 2016, Vienna, Austria, July 4-8, 2016, Proceedings

ISBN

978-3-319-41591-8

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

17

Strana od-do

253-269

Název nakladatele

Springer International Publishing

Místo vydání

Cham

Místo konání akce

Vienna, Austria

Datum konání akce

4. 7. 2016

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

000386263500017