PVS
Specification and Verification System
Dave StringerCalvert
Email:
dave_sc@csl.sri.com
User Group Presentation
Specification and Verification of ASMs in PVS
F. Bartels, A. Dold,
H. Pfeifer, H. Rue§, M. Stegmller, V. Vialard, F. W. v. Henke
Universitt Ulm,
Fakultt fr Informatik,
D89069 Ulm
pvsuser@ki.informatik.uniulm.de
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 ifthenelse 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 highlevel 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 (higherorder) 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
IFTHENELSE.
 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 onestep interpreter
one can apply standard techniques [8, 9] to define traces of
an ASMrun by repetitive application of the onestep 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 onestep interpreter, and two
predicates describing initial and final states, respectively.
We have applied this approach in several case studies. For example, an
ASMbased specification of a compiler backend that generates efficient code
for the DECAlpha architecture has been verified in PVS [10].
Moreover, Brger 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 DLXproof were revealed, and errors in
the code generator specification for DECAlpha 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 coalgebraic concepts, and the two
refinement stepsrefinement via visible states and refinement with
stuttering stepsare derived from a common general refinement principle.
This case study will be explained in more detail in a separate presentation.
 1

Falk Bartels.
Verfeinerung von Zustandsübergangssystemen, ein uniformer
Ansatz basierend auf KoAlgebren.
Master's thesis, Universität Ulm, 1999.
Available at http://www.informatik.uniulm.de/ki/Edu/Diplomarbeiten/fbartelsdipl.html
 2

E. Börger and G. Del Castillo.
A formal method for provably correct composition of a reallife
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 145148, November 1995.
 3

E. Börger and I. Durdanovic.
Correctness of compiling Occam to Transputer code.
Computer Journal, 39(1):5292, 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 489508. NorthHolland, 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 151187.
Springer, 1997.
 6

E. Börger and D. Rosenzweig.
A Mathematical Definition of Full Prolog.
In Science of Computer Programming, volume 24, pages 249286.
NorthHolland, 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 2090. NorthHolland, 1994.
 8

D. Cyrluk.
Microprocessor Verification in PVS: A Methodology and Simple
Example.
Technical Report CSL9312, 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
140149, Hiroshima, Japan, November 1997. IEEE Computer Society.
 10

A. Dold, T. Gaul, V. Vialard, and W. Zimmermann.
ASMBased Mechanized Verification of Compiler BackEnds.
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 157. 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 274309. 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
347362. Springer, 1996.
 14

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

Michael Stegmüller.
Formale Verifikation des DLX RISCProzessors: Eine Fallstudie
basierend auf abstrakten Zustandsmaschinen.
Master's thesis, Universität Ulm, 1998.
Available at http://www.informatik.uniulm.de/ki/Edu/Diplomarbeiten/mstegmuellerdipl.html
 16

K. Stroetmann.
The Constrained Shortest Path Problem: A Case Study In Using ASMs.
Journal of Universal Computer Science, 3(4):304319, 1997.
Dave StringerCalvert (dave_sc@csl.sri.com)