SANDS1.5/COOPN1.5 An Overview of the Language and its Supporting Tools

In this document we give an overview of the CO-OPN/1.5 (Concurrent Object-Oriented Petri Nets) specification language and describe the features of each tool provided in the SANDS/1.5 (Structured Algebraic Net Development System) development environment. The CO-OPN/1.5 language is a specification language devised to support the development of large concurrent systems. The underlying formalisms of the language are algebraic specifications and Petri nets in which tokens correspond to algebraic values. Furthermore, in order to deal with large specifications, some structuring principles have been introduced and in particular, object-orientation paradigm has been adopted for the Petri nets. This means that a CO-OPN/1.5 specification is a collection of objects which interact concurrently. Interaction between the objects is achieved by means of synchronization expressions which allow the designer to select the object interaction policies. The development system provides many different tools such as a syntax checker, a simulator, a property verifier based on temporal logic, a graphic editor, a transformation tool supporting the derivation of specifications, an Ada translator which allows to analyze Ada programs in the CO-OPN/1.5 framework, and a MIMD compiler.