EXECUTABLE SPECIFICATION AND ANALYSIS FOR THE DESIGN OF CONCURRENT OBJECT-ORIENTED SYSTEMS

This paper investigates the analysis of concurrent OO designs using a formal, executable specification technique called G-Net. After presenting an overview of the G-Net technique, we show how to use the G-Net notation to specify the concurrent OO systems. A formal transformation technique, which translates a G-Net specification to a semantically equivalent PrT-net, is presented. The resultant PrT-net can then be formally analyzed. The practical significance of this approach in fault-tolerant systems and distributed multimedia systems design is discussed.