Petri Nets And Algebraic Specifications

The present report covers part of the work carried out in connection to the co-operative project between ENEA and the OECD Halden Reactor Project on graphical and formal methods for software specification. One of the project assignments has been to investigate how graphical descriptions can be supported by the algebraic specification language and associated tool (the HRP Prover) developed at the Halden Project. Since many graphical description languages can be translated to Petri nets, the focus of the investigations has been put on the translation of these nets into algebraic specification. The report introduces two related classes of algebraic specifications, and defines a notion of equivalence between them. It is demonstrated how these two classes provide a suitable framework for the translation of many different types of Petri nets into algebraic specification. It is also demonstrated how this translation makes it possible to analyse the nets with techniques established for algebraic specification, illustrated through the use of the HRP Prover. The exposition in the report contributes to a clarification about the relationship between Petri nets and algebraic specifications. Furthermore, it indicates the extent to which graphical descriptions can be used to explain the meaning of algebraic specifications to non experts. The report also reviews applications of Petri nets related to nuclear power. These include fault diagnosis and fault detection in nuclear reactors, fault tolerance in nuclear reactor protection systems, and modelling of work flow in nuclear waste management. (author)