User Group Meeting

PVS Specification and Verification System

Dave Stringer-Calvert
Email: dave_sc@csl.sri.com

Specification and Verification of ASMs in PVS

The topic of this presentation is the systematic formal treatment of Abstract State Machines (ASMs) and mechanical proof support for the stepwise refinement of ASMs within PVS.

Abstract State Machines, originally known as Evolving Algebras, have become an increasingly popular specification formalism since Gurevich proposed this notion in 1988 [11]. Early work on ASMs focussed on specifying the semantics of programming languages [12, 6, 4] and hardware architectures [3, 2, 5]. More recently, ASMs have been applied to the compilation of programming languages where they are used for both specifying the compilation process and verifying its correctness [7, 3].

An ASM specification basically consists of a set of update rules that describe the operational behaviour of the system under consideration. These update rules are expressed using if-then-else clauses which make the intuitive meaning of ASM specifications easily understandable. An ASM specification essentially denotes a state transition system, and therefore an obvious approach to verifying system properties is that of stepwise refinement starting from a high-level specification and successively providing more refined models. Among the numerous studies on using ASMs for verification only a very few make use of theorem proving tools. Most notably, some of the refinement steps in the compilation of Prolog into WAM code have been mechanically checked with KIV [14] and Isabelle/HOL [13], respectively.

In order to provide mechanical support for ASMs we present a systematic way of expressing ASM specifications in PVS. Using specific features of the PVS language, ASMs can be directly transformed into PVS specifications, in particular:

• Universes. ASMs sorts are introduced by means of unary relations. As PVS includes a powerful type system, universes can directly be modeled through uninterpreted PVS types. Refinement of universes is accomplished by instantiation of corresponding theory parameters.
• Static functions are not changed by the update rules of an ASM and can thus be modeled by ordinary PVS functions.
• Dynamic functions are subject to changes via the update rules and are modeled as (higher-order) components of a record type that reflects the state of an Abstract State Machine.
• Update rules change the value of dynamic functions at particular arguments. In PVS these rules are easily expressed by record updates via the WITH construct. Updates can be simultaneous or nested, and conditional rules are handled in the obvious manner using IF-THEN-ELSE.
• External functions describe aspects of the environment of an ASM and can be modeled as theory parameters with the intended meaning or required properties being supplied by theory assumptions. Again, refinement of external functions is done by instantiating theory parameters.

The operational behaviour of an ASM is given by a sequence of states; each state is obtained from its predecessor by executing all applicable update rules. Given that the update rules are combined into a one-step interpreter one can apply standard techniques [8, 9] to define traces of an ASM-run by repetitive application of the one-step interpreter. This concept is independent of a concrete ASM and can be modeled by a generic PVS theory that is parameterized by the state type, the one-step interpreter, and two predicates describing initial and final states, respectively.

We have applied this approach in several case studies. For example, an ASM-based specification of a compiler back-end that generates efficient code for the DEC-Alpha architecture has been verified in PVS [10]. Moreover, Bšrger and Mazzanti's treatment of the RISC architecture DLX [5] has been formally analysed and a refinement from a sequential model of DLX into the pipelined DLX has been verified [15]. In both cases proof strategies have been defined that accomplish most of the proofs fairly automatically. Additional benefit of these formal verifications is that implicit details of the original DLX-proof were revealed, and errors in the code generator specification for DEC-Alpha could be found through the failure of proof attempts.

Recently, the derivation of two algorithms for determining the shortest path in a graph under certain constraints [16] by stepwise refinement has been verified [1]. Both the problem specification and the algorithms are given as ASMs and the algorithms are shown to be successive refinements of the abstract specification. Here, the traces of ASM runs are defined using sequences that are based on co-algebraic concepts, and the two refinement steps--refinement via visible states and refinement with stuttering steps--are derived from a common general refinement principle. This case study will be explained in more detail in a separate presentation.

References

1

Falk Bartels. Verfeinerung von Zustandsübergangssystemen, ein uniformer Ansatz basierend auf Ko-Algebren. Master's thesis, Universität Ulm, 1999. Available at http://www.informatik.uni-ulm.de/ki/Edu/Diplomarbeiten/fbartels-dipl.html

2

E. Börger and G. Del Castillo. A formal method for provably correct composition of a real-life processor out of basic components (The APE100 Reverse Engineering Study). In B. Werner, editor, Proceedings of the First IEEE International Conference on Engineering of Complex Computer Systems (ICECCS'95), pages 145-148, November 1995.

3

E. Börger and I. Durdanovic. Correctness of compiling Occam to Transputer code. Computer Journal, 39(1):52-92, 1996.

4

E. Börger, I. Durdanovic, and D. Rosenzweig. Occam: Specification and Compiler Correctness. Part I: Simple Mathematical Interpreters. In U. Montanari and E. R. Olderog, editors, Proc. PROCOMET'94 (IFIP Working Conference on Programming Concepts, Methods and Calculi), pages 489-508. North-Holland, 1994.

5

E. Börger and S. Mazzanti. A Practical Method for Rigorously Controllable Hardware Design. In J.P. Bowen, M.B. Hinchey, and D. Till, editors, ZUM'97: The Z Formal Specification Notation, volume 1212 of LNCS, pages 151-187. Springer, 1997.

6

E. Börger and D. Rosenzweig. A Mathematical Definition of Full Prolog. In Science of Computer Programming, volume 24, pages 249-286. North-Holland, 1994.

7

E. Börger and D. Rosenzweig. The WAM - Definition and Compiler Correctness. In C. Beierle and L. Plümer, editors, Logic Programming: Formal Methods and Practical Applications, Studies in Computer Science and Artificial Intelligence, chapter 2, pages 20-90. North-Holland, 1994.

8

D. Cyrluk. Microprocessor Verification in PVS: A Methodology and Simple Example. Technical Report CSL-93-12, SRI International, Computer Science Laboratory, December 1993.

9

David Cyrluk, John Rushby, and Mandayam Srivas. Systematic Formal Verification of Interpreters. In Michael G. Hinchey and Shaoying Liu, editors, First International Conference on Formal Engineering Methods (ICFEM '97), pages 140-149, Hiroshima, Japan, November 1997. IEEE Computer Society.

10

A. Dold, T. Gaul, V. Vialard, and W. Zimmermann. ASM-Based Mechanized Verification of Compiler Back-Ends. In Proceedings of the 28th Annual Conference of the German Society of Computer Science. Technical Report, Magdeburg University, 1998.

11

Y. Gurevich. Logic and the Challenge of Computer Science. In E. Börger, editor, Current Trends in Theoretical Computer Science, pages 1-57. Computer Science Press, 1988.

12

Y. Gurevich and J. Huggins. The Semantics of the C Programming Language. In E. Börger, H. Kleine Büning, G. Jäger, S. Martini, and M. M. Richter, editors, Computer Science Logic, volume 702 of LNCS, pages 274-309. Springer, 1993.

13

C. Pusch. Verification of compiler correctness for the WAM. In J.Harrison J. von Wright, J.Grundy, editor, Theorem Proving in Higher Order Logics (TPHOLs'96), volume 1125 of LNCS, pages 347-362. Springer, 1996.

14

G. Schellhorn and W. Ahrendt. Reasoning about Abstract State Machines: The WAM Case Study. Journal of Universal Computer Science, 3(4):377-413, 1997.

15

Michael Stegmüller. Formale Verifikation des DLX RISC-Prozessors: Eine Fallstudie basierend auf abstrakten Zustandsmaschinen. Master's thesis, Universität Ulm, 1998. Available at http://www.informatik.uni-ulm.de/ki/Edu/Diplomarbeiten/mstegmueller-dipl.html

16

K. Stroetmann. The Constrained Shortest Path Problem: A Case Study In Using ASMs. Journal of Universal Computer Science, 3(4):304-319, 1997.