ASM2000 Gargantini, Angelo Riccobene, Elvinia

Encoding Abstract State Machines in PVS

in Abstract State Machines, Theory and Applications, International Workshop, ASM 2000, Monte Verita', Switzerland, March 19-24, 2000, Proceedings. (Eds. Gurevich, Yuri and Kutter, PhilippW. and Odersky, Martin and Thiele, Lothar) , Springer Berlin Heidelberg, Lecture Notes in Computer Science, vol. 1912 (2000): 303-322 ISBN 978-3-540-67959-2

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 \citeBoeMea97 is taken as case study to show how to formalize multi-agent ASMs in PVS and prove properties.

[download the pdf file] [DOI]

My sw links