From Formal Specifications to Ready-to-Use Software Components: The Concurrent Object-Oriented Petri Net Approach

CO-OPN (Concurrent Object Oriented Petri Net) is a formal specification language for modelling distributed systems; it is based on coordinated algebraic Petri nets. In this paper we describe a method for generating an executable prototype from a CO-OPN specification. We focus our discussion on the generation of executable code for CO-OPN classes. CO-OPN classes are defined using Petri Nets. The main problems arise when implementing synchronization and non-determinism of CO-OPN classes in procedural languages. Our method proposes a solution to these problems. Another interesting aspect of our method is the easy integration of a generated prototype into any existing system. This paper focuses on the generation of Java code that fulfils the Java Beans component architecture, however our approach is also applicable to other object-oriented implementation languages with a component architecture.

COOPN/2 : A Specification Language for Distributed Systems Engineering

In this article we present the concurrent object-oriented specification language COOPN/2 which extends the COOPN (Concurrent Object Oriented Petri Nets) formalism, destined to support the development of large heterogenous distributed systems. The development of distributed applications has recently been the subject of intensive research, due to potential benefits that can be expected to offer in increasing reliability and overall performance of computer processing. One way of improving the effectiveness of the distributed system construction is to adopt a rigorous approach for system development, based on structuring principles. The COOPN/2 approach proposes a specification language, based on the object-oriented paradigm, which includes a fine description of true concurrent behaviors. This hybrid approach (model and property-oriented) allows for a description of the concurrent aspects through the use of a high-level Petri nets formalism which includes data structures expressed with the algebraic abstract data types and a synchronization mechanism for building hierarchies of abstraction. This latter notion is the concept which is used in structuring applications. Interesting properties of COOPN, such as the progressive refinement of specifications, allow for the building of systems in an incremental manner.In this article, we introduce COOPN/2 informally, by means of a typical example of distributed systems, the transit node, in order to introduce each useful and innovative mechanism of the language. Then, in the context of distributed software engineering with COOPN/2, we present our current works done in order to provide formal methods for several steps of a life cycle model test, prototyping, analysis,....). Keywords: software engineering, formal specification language, refinement, prototyping, distributed systems, object orientation, concurrency, Petri nets, algebraic specification.

1996

Formal Development of Java Programs

The Java object-oriented programming language has been the subject of an important involvement from programmers and industry. Especially for applications related to the Web. The problem of such rapid penetration of Java programs into commercial product is that software engineers does not have any methodology and have to develop complex parallel applications. In this paper, we present, using a real (http://lglsun.epfl.ch/Team/GDM/DSGamma.html) but simple Web parallel application, a possible formal development methodology based on the stepwise refinement of CO-OPN/2 formal specifications. The application chosen is based on the Gamma paradigm, in which additions are realized across distributed multisets of integers maintained by local Java applets. CO-OPN/2 is an object-oriented specification formalism allowing the formal specification of abstract data types based on algebraic specification and of concurrent objects using a Petri net like approach. An interesting feature of CO-OPN/2 is that it gives a coherent solution for the expression of complex properties combining inheritance, concurrency and synchronizations. The refinement of formal descriptions for building progressively the Java program is presented in several refinement steps. This refinement process focuses on the distribution of data and treatments, and validation and verification are studied through the refinement of system properties.

1997

An incremental prototyping methodology for distributed systems based on formal specifications

This thesis presents a new incremental prototyping methodology for formally specified distributed systems. The objective of this methodology is to fill the gap which currently exists between the phase where a specification is simulated, generally using some sequential logical inference tool, and the phase where the modeled system has a reliable, efficient and maintainable distributed implementation in a main-stream object-oriented programming language. This objective is realized by application of a methodology we call Mixed Prototyping with Object-Orientation (in short: OOMP). This is an extension of an existing approach, namely Mixed Prototyping, that we have adapted to the object-oriented paradigm, of which we exploit the flexibility and inherent capability of modeling abstract entities. The OOMP process proceeds as follows. First, the source specifications are automatically translated into a class-based object-oriented language, thus providing a portable and high-level initial implementation. The generated class hierarchy is designed so that the developer may independently derive new sub-classes in order to make the prototype more efficient or to add functionalities that could not be specified with the given formalism. This prototyping process is performed incrementally in order to safely validate the modifications against the semantics of the specification. The resulting prototype can finally be considered as the end-user implementation of the specified software. The originality of our approach is that we exploit object-oriented programming techniques in the implementation of formal specifications in order to gain flexibility in the development process. Simultaneously, the object paradigm gives the means to harness this newly acquired freedom by allowing automatic generation of test routines which verify the conformance of the hand-written code with respect to the specifications. We demonstrate the generality of our prototyping scheme by applying it to a distributed collaborative diary program within the frame of CO-OPN (Concurrent Object-Oriented Petri Nets), a very powerful specification formalism which allows expressing concurrent and non-deterministic behaviours, and which provides structuring facilities such as modularity, encapsulation and genericity. An important effort has also been accomplished in the development or adaptation of distributed algorithms for cooperative symbolic resolution. These algorithms are used in the run-time support of the generated CO-OPN prototypes.

EPFL1997

An incremental prototyping methodology for distributed systems based on formal specifications

EPFL1997