Object-oriented software development, formal verification, formal methods, stepwise refinement, Java

Giovanna Di Marzo Serugendo

Prof. Alfred Strohmeier

The stepwise refinement of formal system specifications is a technique that consists of gradually transforming an abstract system specification, in order to let it take into account more and more implementation constraints. After a series of refinement steps, a concrete system specification is reached that describes an operational model of the system, and takes into account the constraints of the execution environment (programming language, execution platform, etc.). The concrete system specification should of course respect the abstract system specification and as well the requirement specification. In the case of model-oriented specification the verification that a refinement step is correct is a difficult task and usually follows an informal way.

In order to enable formal verification of stepwise refinement steps, this thesis provides a definition of stepwise refinement, of model-oriented specifications, that is based on the use of an additional logical language. Essential properties that have to be preserved during a refinement step are explicitly expressed using logical formulae. This set of formulae is called a contract. A refinement step is then defined as the replacement of a high-level contractual specification by a lower-level one that preserves the contract of the higher-level one. Properties that are not part of the contract may be lost during a refinement step.

According to these principles, a general theory of refinement and implementation based on contracts has been defined for model-oriented specifications languages and logical languages. The general theory of refinement and implementation based on  contracts has been applied to the CO-OPN/2 formal specifications language; the Hennessy-Milner logic (HML) is used for expressing the contracts on CO-OPN/2 specifications. Attention has been given to refinement processes ending with an implementation phase using the Java programming language.

Future work is related to: (1) the assessment of the general theory by applying it to other model-oriented specifications languages; (2) the enhancement of HML formulae; (3) the development of tools assisting the specifying during the refinement process.

The contributions of this thesis are the following:

• A general theory of :
• stepwise refinement based on the use of contracts;
• implementation based on the use of contracts;
• The application of these theories to the CO-OPN/2 language, in order to provide:
• a theory of stepwise refinement of CO-OPN/2 specifications;
• a theory of implementation of CO-OPN/2 specifications;
• A development methodology for CO-OPN/2 which provides:
• a formal development process (anlaysis, design, implementation) for distributed applications;
• a development method of Java applications;
• the use of test generation in order to perform verifications.

Giovanna Di Marzo Serugendo and Nicolas Guelfi, ``Formal Development of Java Based Web Parallel Applications,'' Proceedings of the Hawaii International Conference on System Sciences (HICSS-31), IEEE Computer Society Press, 1998.

Giovanna Di Marzo Serugendo and Nicolas Guelfi, ``Using Object-Oriented Algebraic Nets for the Reverse Engineering of Java Programs: A Case Study,'' Proceedings of the International Conference on Application of Concurrency to System Design (CSD'98), IEEE Computer Society Press, 1998.

G. Di Marzo Serugendo, N. Guelfi, A. Romanovsky and A. Zorzo, ``Formal Development and Validation of the DSGamma System Based on CO-OPN/2 and Coordinated Atomic Actions,'' Technical Report 98/265, Sotware Engineering Laboratory, Swiss Federal Institute of Technology, Lausanne, Switzerland, 1998.

Giovanna Di Marzo Serugendo, ``Stepwise Refinement of Formal Specifications Based on Logical Formulae: from CO-OPN/2 Specifications to Java Programs,'' Ph.D. Thesis, no 1931, Ecole Polytechnique Fédérale de Lausanne, Département d'informatique, CH-1015 Lausanne, Switzerland, 1999.