In: J.W. de Bakker, et al.: Lecture Notes in Computer Science, Vol. 430; Proceedings of the REX Workshop on Stepwise Refinement, 1989, Mook, The Netherlands, pages 180-207. Berin, Germany: Springer-Verlag, 1990.
Abstract: In the paper, the questions of reactive behaviour decomposition and stepwise refinement are considered using a particular class of Petri nets as models for open reactive systems. The paper presents an assumption/commitment style temporal logic for specifying the behaviour of such systems, an automatic proof method for verifying the correctness of an implementation of such a specification in terms of the considered class of Petri nets based on modelchecking of MCTL formula, and presents a proof method for infering the behaviour of a compound reactive system from the behaviour of its constituents.
Keywords: modular verification; temporal logic; refinement; reactive system.