Formal Development and Validation of the DSGamma System Based on CO-OPN/2 and Coordinated Atomic Actions

The objectives of this research are twofold. On the first hand, it aims to show the interest of Coordinated Atomic actions (CA actions) as a design concept and, on the other hand it explains how the formal language COOPNTWO can be used to express a CA action design. A real distributed application is developed according to a simple development life cycle: informal requirements, specification, design, implementation. The design phase is built according to the CA action concept. The COOPNTWO language is used to express the specification, and design phase. The implementation is made in Java based on a library of generic classes adapted to CA action concepts. The validation phase is briefly addressed, in order to demonstrate the extent to which the development methodology followed in this paper can be useful for proving properties.