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.

Formal testing of object-oriented software

Cécile Peraire

This thesis presents a method and a tool for test set selection, dedicated to object-oriented applications and based on formal specifications. Testing is one method to increase the quality of today's extraordinary complex software. The aim is to find program errors with respect to given criteria of correctness. In the case of formal testing, the criterion of correctness is the formal specification of the tested application: program behaviors are compared to those required by the specification. In this context, the difficulty of testing object-oriented software arises from the fact that the behavior of an object does not only depend on the input values of the parameters of its operations, but also on its current state, and generally on the current states of other related objects. This combinatorial explosion requires carefully selecting pertinent test sets of reasonable size. This thesis proposes a formal testing method which takes this issue into account. Our approach is based on two different formalisms: a specification language well adapted to the expression of system properties from the specifier's point of view, and a test language well adapted to the description of test sets from the tester's point of view. Specifications are written in an object-oriented language, CO-OPN (Concurrent Object-Oriented Petri Nets), based on synchronized algebraic Petri nets and devoted to the specification of concurrent systems. Test sets are expressed using a very simple temporal logic, HML (Hennessy-Milner Logic), whose logic formulas can be executed by a program. There exists a full agreement, shown in this thesis, between the CO-OPN and HML satisfaction relationships: the program satisfies its specification if and only if it satisfies the exhaustive test set derived from this specification. The exhaustive test set expresses all the specification properties. The exhaustive test set is generally infinite. Its size is reduced by applying hypotheses to the program behavior. These hypotheses define test selection strategies and reflect common test practices. The quality of the test sets thus selected only depends on the pertinence of the hypotheses. Concretely, the reduction is achieved by associating to each hypothesis applied to the program, a constraint on the test set. Our method proposes a set of elementary constraints: syntactic constraints on the structure of the tests and semantic constraints which allow to instantiate the test variables so as to cover the different classes of behaviors induced by the specification (subdomain decomposition). Elementary constraints can be combined to form complex constraints. Finally, the constraint system defined on the exhaustive test set is solved, and the solution leads to a pertinent test set of reasonable size. Thanks to the CO-OPN semantics, which allows to compute all the correct and incorrect behaviors induced by a specification, our method is able to test, on the one hand that a program does possess correct behaviors, and on the other hand that a program does not possess incorrect behaviors. An advantage of this approach is to provide through the tests, an observational description of valid and invalid implementations. Our testing method exhibits the advantage of being formal, and thus allows a semi-automation of the test selection process. A new tool, called CO-OPNTEST, is presented in this thesis. This tool assists the tester during the construction of constraints to apply to the exhaustive test set; afterward it automatically generates a test set satisfying these constraints. The CO-OPNTEST architecture is composed of a PROLOG kernel and a Java graphical interface. The kernel is an equational resolution procedure based on logic programming. It includes control mechanisms for subdomain decomposition. The graphical interface allows a user-friendly definition of the test constraints. The CO-OPNTEST tool has generated test sets for several case studies in a simple, rapid and efficient way. In particular, it has generated test sets for an industrial case study of realistic size: the control program of a production cell [Lewerentz 95]. CO-OPNTEST and its application to significant examples demonstrate the pertinence of our approach.

EPFL1998

SANDS: Structured Algebraic Net Development System

SANDS is a development tool based on structured algebraic nets. The environment is composed of the following features: - Algebraic nets allowing the definition and use of structured tokens by means of algebraic specifications. Apart from reducing the size of a model these nets are accurate in describing data transformations during the evolution of the system being modelled; - Structured nets necessary for large system developments. The latter two components form together the language used and understood by the environment. The development environment provides the user with an application simulation tool. This component provides immediate views of any modifications brought to the system being modelled. The environment also permits modifications to the automatically generated code through manual insertions or deletions of C or Prolog instructions. Model semantics possess a well formalized underlying theory. Connections with other theories are numerous and offer a large range of possibilities for describing and proving properties about systems. We can mention amongst other rewriting systems, bisimulation (behaviour comparison between two system models), refinement of objects, algebraic specifications and proof of temporal logic properties used as a more abstract specification language. The user builds and structures his model as a set of algebraic nets called 'objects' representing either instances or classes depending on the context of the modelling. These objects are related to each other by synchronization links which determine and limit the way the objects can evolve concurrently. Algebraic specifications and objects can be used in three different ways: they can be generic, 'ground' or instantiated. The underlying model, namely CO-OPN (Concurrent Object-Oriented Petri Nets), is described in more depth in: 'CO-OPN: A Concurrent Object- Oriented Petri Nets' International Conference on Application and Theory of Petri Nets, Aarhus June 1991. SANDS has two main components: the CO-OPN graphical editor and the simulation tool. Both parts are independent in the following sense: the user can develop his model inside the graphical editor and call the simulation tool from the editor, on the other hand he can use the CO-OPN specification language to describe his model in a textual way and then use the simulation tool after having verified the validity of the specification with the compiler. Moreover these possibilities can be mixed. The user can also modify the specifications by editing the file generated by the graphical editor (written in the CO-OPN language). The graphical tool can be avoided, if desired, through hand written specifications describing the model; a specification made in the CO-OPN language can also be loaded and then modified in the graphical environment. The specifications obtained can then be simulated once the compilation and linking phases have been successfully achieved. The compiling and linking can be performed through the grap The algebraic specification of data can be defined outside of the graphical editor environment. When this has been done the latter specifications can be imported in the graphical editor where their signatures are graphically represented. This set of algebraic specifications are used as a basis which support object specifications. There is no constraint on the way the user builds his specifications. He can adopt a top-down or a bottom-up methodology. Therefore the user can set the overall objects distribution in order to structure his model and then define the behaviour of each object. On the othe hand he can build his application on a set of objects already defined. However, these approaches can also be mixed.

1993

Stepwise refinement of formal specifications based on logical formulae

One of the steps making it possible to increase the quality and the reliability of the software executing on distributed systems consists of the use of methods of software engineering that are known as formal. The majority of the formal methods currently existing correspond in fact more to formal specifications languages than to methods themselves. This is due to the fact that the two fundamental aspects which are: the logic of use of the language and the coverage of the software life cycle are not, for the majority, defined. The development by stepwise refinement is one of the means making it possible to define these two aspects. This thesis aims to the definition of the concepts of refinement and implementation of model-oriented formal specifications. It brings a methodological base making it possible to use such a specifications language during a development by stepwise refinements and during the implementation stage. This thesis defines, initially, a theoretical framework for the refinement and the implementation of formal specifications. The main idea consists in associating a contract with each specification. A contract explicitly represents the whole of the properties of the specification which it is necessary to preserve at the time of a refinement of this specification. To show that a concrete specification refines some abstract specification, it is then a matter of showing that the contract of the concrete specification is sufficient to ensure the properties corresponding to the contract of the abstract specification. The second part of this thesis consists in applying this theoretical framework in the context of the CO-OPN/2 language. CO-OPN/2 is an object-oriented formal specifications language founded on algebraic specifications and Petri nets. Thus, definitions of the concepts of contracts, refinement and implementation are proposed for this language. The contracts are expressed using the Hennessy-Milner temporal logic (HML). This logic is used in the theory of test provided with language CO-OPN/2. Thus, the verification of the contractual properties, as well as the verification of the stages of refinement are facilitated. Refinement and implementation are controlled semantically by the satisfaction of the contracts; syntactically, a renaming is authorised. We specifically study the implementation using the Java programming language. We show how to specify classes of the Java programming language using language CO-OPN/2, so that the last stage of the process of refinement leads to a specification entirely built using CO-OPN/2 components specifying Java classes. The stage of implementation in the Java language itself is thus facilitated. The third part of this thesis shows how it is possible to practically verify that a CO-OPN/2 specification satisfies its own contract, that a stage of refinement is correctly carried out, and finally that the stage of implementation is correctly performed. These verifications are carried out using the theory of the test provided with language CO-OPN/2. Finally, the last part of this thesis illustrates the cogency of this approach by applying it to a complete and detailed case study. A distributed Java application is developped according to the method introduced for the CO-OPN/2 language. Refinement is guided mainly by the satisfaction of functional requirements and by constraints of design integrating the concept of client/server architecture. Lastly, the stages chosen in the refinement process of this development make it possible to study aspects specific to distributed applications, and to propose generic schemas for the design of such applications.

EPFL1999