SMT-based automatic proof of ASM model refinement

Result code in 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>
Result on the web
<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>

Result language
angličtina
Original language name
SMT-based automatic proof of ASM model refinement
Original language description
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.
Czech name
—
Czech description
—

Project
<a href="/en/project/GA14-11384S" target="_blank" >GA14-11384S: Automatic Formal Analysis and Verification of Programs with Complex Unbounded Data and Control Structures</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

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

Article name in the collection
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
—
Number of pages
17
Pages from-to
253-269
Publisher name
Springer International Publishing
Place of publication
Cham
Event location
Vienna, Austria
Event date
Jul 4, 2016
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
000386263500017

Similar results(10)