Exploiting Various Levels of Semantics in CO-OPN for the SANDS Environment Tools

This paper describes the techniques and tools developed to support the construction of CO-OPN specifications (Concurrent Object Oriented Petri Nets) [7] and the kind of semantics that are needed for each part of the environment. CO-OPN is a specification language which permits an abstract description of aspects of concurrent operations and data-structures of computer programs. The concurrent and operational part of the formalism is described by means of Petri nets, while the data-structures are described by means of algebraic abstract data types. In the CO-OPN formalism, these associations are structured with the notion of objects. CO-OPN specifications can be developed, analyzed and simulated in a dedicated environment called SANDS (Structured Algebraic Nets Development System [6]). Various semantics of CO-OPN are exploited: an abstract operational semantics is used for the logic programming simulator as well as for the test set generation tool, while a more concrete operational semantics based on transactions is necessary for prototyping on distributed systems. All these semantics are valid and partially complete on a subpart of the CO-OPN language with respect to its denotational semantics.