Abstract State Machines (ASMs) represent a general model of computation which subsumes all other classic computational models. Since the notion of ASM state naturally captures the classic notion of program state, ASMs are suitable to be verified through a predicate abstraction approach. The aim of this paper is to discuss how predicates over ASM states can support the formal verification of ASM-based models. The proposal can overcome the main limitations that penalize traditional model checking techniques applied to ASMs.
Applying Predicate Abstraction to Abstract State Machines
BIANCHI, Alessandro;PIZZUTILO, Sebastiano;VESSIO, GENNARO
2015-01-01
Abstract
Abstract State Machines (ASMs) represent a general model of computation which subsumes all other classic computational models. Since the notion of ASM state naturally captures the classic notion of program state, ASMs are suitable to be verified through a predicate abstraction approach. The aim of this paper is to discuss how predicates over ASM states can support the formal verification of ASM-based models. The proposal can overcome the main limitations that penalize traditional model checking techniques applied to ASMs.File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
