SMT for state-based formal methods: the ASM case study

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F18%3A10374942" target="_blank" >RIV/00216208:11320/18:10374942 - isvavai.cz</a>

Výsledek na webu

<a href="https://doi.org/10.29007/djdz" target="_blank" >https://doi.org/10.29007/djdz</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.29007/djdz" target="_blank" >10.29007/djdz</a>

Jazyk výsledku

angličtina

Název v původním jazyce

SMT for state-based formal methods: the ASM case study

Popis výsledku v původním jazyce

State-based transition systems can take advantage of a symbolic representation of the concepts of state and transition in order to automatically solve verification questions that could not be otherwise tackled in terms of explicit representation of the transition system. We report here our experience in developing solutions, approaches and supporting tools of verification problems regarding the Abstract State Machines (ASMs), a transition system which can be considered as an extension of Finite State Machines. We present the symbolic representation of an ASM and of its computational model in terms of the Yices SMT solver. We also discuss two scenarios of verification questions regarding the ASMs for which the symbolic representation helped us to formalize and solve the problem by satisfiability checking, namely automatic proof of correct ASM refinement and runtime verification.

Název v anglickém jazyce

SMT for state-based formal methods: the ASM case study

Popis výsledku anglicky

State-based transition systems can take advantage of a symbolic representation of the concepts of state and transition in order to automatically solve verification questions that could not be otherwise tackled in terms of explicit representation of the transition system. We report here our experience in developing solutions, approaches and supporting tools of verification problems regarding the Abstract State Machines (ASMs), a transition system which can be considered as an extension of Finite State Machines. We present the symbolic representation of an ASM and of its computational model in terms of the Yices SMT solver. We also discuss two scenarios of verification questions regarding the ASMs for which the symbolic representation helped us to formalize and solve the problem by satisfiability checking, namely automatic proof of correct ASM refinement and runtime verification.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

<a href="/cs/project/GA17-12465S" target="_blank" >GA17-12465S: Verifikace a hledání chyb v pokročilém softwaru</a><br>

Návaznosti

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

Rok uplatnění

2018

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

Automated Formal Methods

ISBN

—

ISSN

2515-1762

e-ISSN

neuvedeno

Počet stran výsledku

18

Strana od-do

1-18

Název nakladatele

EasyChair

Místo vydání

Neuveden

Místo konání akce

Moffett Field, CA, USA

Datum konání akce

19. 5. 2017

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

WRD - Celosvětová akce

Kód UT WoS článku

—