DESCRIBING AND VERPIYING SYSTEMS: A COMPOSITIONAL UEBRA FOR PETRI NETS
Robert Zirnmer, Alan MacDonald, Robert A. Hoke · 1992
In this paper we describe a method for composing Petri Nets. This is an application of a general categorical composition algebra which we describe elsewhere. We use the example of a three-wire handshake to illustrate some features of this Petri Net composition. Tntroduction We are designing a CAD system the circuits designed in which will be automatically provably-correct implementations of their initial specifications. The system we have in mind will have a predicate logic theorem prover at its core and will mirror every surface-level design step with an internal proof-step; for a discussion of the general technique see [l]. However, some aspects of high-level circuit requirements are difficult to describe in Predicate Logic. We have found that Petri Nets can be useful models for some of these, such as concurrency and timing considerations. Incorporating Petri Nets in a proof-based CAD environment raises two problems: adding Pem Nets could destroy the mathematical integrity of the system and Petri Net descriptions of anything but the simplest systems are large and difficult to work with. We have solved both of these problems by using a general-purpose composition algebra. The integrity is ensured by insisting that all of the translations are homomorphisms (that is, functions that respect the structure of the composition algebra) and that the Petri Nets are themselves verified; the descriptions are made tractable because the composition algebra allows us to define large Petri Nets by describing a sequence of small nets and the relations between these nets. In this paper we use the example of a three-wire handsh&e (from the IEEE 488 / IEC 625 instrumentation bus standard) to show several different aspects of the composition algebra, and how it can be used to express aspects of hardware specification and design that are very difficult to express in other formal models of concurrency. We will also explain how we can use these algebraic notions to verify system specifications. This complements most formal methods work (and indeed the CAD system described above) which concerns designing circuits that are provably correct implementations of assumed adequate specifications. braic CAD and Integration of Formal Methods.