In: Proceedings of the 16th Australian Computer Science Conference, Brisbane, Australia, pages 765-772. 1993.
Abstract: LOOPN is a language and simulator for specifying systems in terms of coloured timed petri nets. It includes object-oriented features such as subtyping, inheritance and polymorphism which allow for the convenient modularisation of complex specifications. This paper examines the issue of modular correctness, and the extent to which the traditional invariant analysis of petri nets is applicable. In doing so, it considers the proposals for calculating modular place flows proposed by Christensen and Petrucci. It also discusses the limitations of invariant analysis as identified by Reisig. The paper illustrates these ideas with the standard producer-consumer problem and a sliding window protocol.