A formal protocol specification with predicate/transition nets

The Petri Net Theory provides a method for the formal specification of concurrent systems (e.g. distributed computer systems for diagnostic- and shutdown functions in Fast Reactors). This method includes the verification/validation of the net specification about the causal behavior of the modeled concurrent system. Especially the predicate/transition nets (very important class of high level nets) provide very compact net specifications. Additionally, a predicate/transition net can be described by different levels of a system abstraction (for example in form of a net morphism). So it is possible to describe a concurrent system in a formal manner and to validate its causal behavior already during the design phase in the software live cycle. For example it can be shown, that all global states of an application protocol do not include deadlocks and livelocks. Formal net specifications and the results of their analysis raise the reliability of software systems themselves and also the quality of the software documentation. For the verification and documentation of net specifications computer tools are an absolute necessity. In our case the operating system UNIX is available with a special Petri Net Tool PROVER (PRedicate/Transition Net Oriented VERification System). In this environment a net specification was developed which provides a formal description of an application protocol for a communication system. This communication system is the central part of our distributed Fast Reactor Diagnostic System DESYRE (Diagnostic Expert SYstem for REactor Surveillance)