Abstract
In this paper we show how the Specification and verification system PVS (Prototype Verification System) can provide tool support for Abstract State Machines (ASMs), especially oriented towards automatic proof checking and mechanized proving of properties. Useful templates are presented which allow encoding of ASM models into PVS without any extra user's skill. We prove the transformation preserves the ASM semantics and provide a framework for an automatic tool, prototypically implemented, which translates ASM Specifications in PVS. The ASM Specification of the Production Cell given in [4] is taken as case study to show how to formalize multi-agent ASMs in PVS and prove properties. © Springer-Verlag Berlin Heidelberg 2000.
Cite
CITATION STYLE
Gargantini, A., & Riccobene, E. (2000). Encoding abstract state machines in PVS. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1912 LNCS, pp. 303–322). Springer Verlag. https://doi.org/10.1007/3-540-44518-8_17
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
