Generation of object-oriented programs from CO-OPN specifications

The execution of formal specifications is important for verification, validation and animation purposes. This thesis describes transformation of CO-OPN specifications in executable code. The original goal of this transformation was validation by prototyping, but animation and, partially, verification also became interesting goals during the development. The work was already done to study the transformation of CO-OPN specifications to Prolog programs [18], to ADA programs [37] and even to Java programs [57]. Nevertheless the only implemented technique was the transformation to Prolog. Starting with those results, we designed and implemented the automatic transformation of CO-OPN specifications to Java programs. The main contributions of this work are: Definition and implementation of CO-OPN state and execution models. Study and implementation of various methods to integrate generated code with external systems. Implementation of an extensible code generator. This thesis first gives a brief introduction to CO-OPN language, then describes main principles that govern the transformation of CO-OPN to executable code. This explanation is logically divided in three parts, corresponding to main CO-OPN entities: generation of Abstract Data Types, Classes and Contexts. Then the architecture of code generation engine is presented. Finally, integration of generated code is illustrated by comprehensive examples.