Prototyping and analysis of non-sequential systems using predicate-event nets
The specification language SEGRAS is centered on Predicate-Event nets (PrE-nets), a class of Petri nets with data tokens of an abstract data type. The data flowing in these nets and the firing constraints are specified using algebraic specification. The Petri net specifies the behavioral aspects: the specification of data distribution and synchronization of function calls. PrE-nets inherit from the algebraic theory of abstract data types and from net-theory; from the former, modular composition, information hiding, reasoning about consistency of specifications and correctness of implementations, which is a weakness of standard Petri nets; from the latter they inherit a natural graphical presentation of parallel activity and foremost a rich theoretically founded set of methods for simulating and analyzing the dynamic behavior of systems and the interaction of their components. This paper gives a short formal introduction into the theory of PrE-nets, relates the algebraic semantics to the net-semantics and illustrates this relation informally by sketching the simulation methods we have developed for these nets in the ESPRIT-project GRASPIN. The paper then presents some recent theoretical results with respect to the liveness and safeness of these nets and gives examples how these can be used in a specification environment that includes net transformation and decomposition.