Authors: Alessandro Bianchi, Gennaro Vessio, Sebastiano Pizzutilo
Tags: 2015, conceptual modeling
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.Read the full paper here: https://link.springer.com/chapter/10.1007/978-3-319-19237-6_18
