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.
SMT for state-based formal methods: the ASM case study / P. Arcaini, A. Gargantini, E. Riccobene: - In: Automated Formal Methods / [a cura di] N. Shankar, B. Dutertre. - Prima edizione. - [s.l] : Kalpa Publications in Computing, 2018. - pp. 1-18
SMT for state-based formal methods: the ASM case study
P. Arcaini;E. Riccobene:
Co-primo
2018
Abstract
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.File | Dimensione | Formato | |
---|---|---|---|
SMT_for_state-based_formal_methods_the_ASM_case_study.pdf
accesso riservato
Tipologia:
Publisher's version/PDF
Dimensione
532.15 kB
Formato
Adobe PDF
|
532.15 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.