Technical report
OA Policy
English

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

MandatorSoftware Engineering Laboratory, Swiss Federal Institute of Technology
Number of pages24
PublisherLausanne : Software Engineering Laboratory, Swiss Federal Institute of Technology
Publication date1998
Abstract

The rapid expansion of Java programs into software market is often not supported by a proper development methodology. Here, we present a formal development methodology well-suited for Java dependable distributed applications. It is based on the stepwise refinement of model-oriented formal specifications, and enables validation of the obtained system wrt the client's requirements. Three refinement steps have been identified in the case of fault-tolerant distributed applications: first, starting from informal requirements, an initial formal specification is derived. It does not depend on implementation constraints and provides a centralized solution, second, dependability and distribution constraints are integrated; third, the Java implementation is realised. The CO-OPN/2 language is used to express specifications formally; and the dependability and distribution design is based on the Coordinated Atomic action concept. The methodology and the three refinement steps are presented through a very simple fault-tolerant distributed Java application.

Keywords
  • Structuring complex concurrent systems
  • CO-OPN/2
  • Formal development
  • Stepwise refinement
  • Design for validation
  • Coordinated atomic actions
  • Java
Citation (ISO format)
DI MARZO SERUGENDO, Giovanna et al. Formal Development and Validation of the DSGamma System Based on CO-OPN/2 and Coordinated Atomic Actions. 1998
Main files (1)
Report
accessLevelPublic
Identifiers
  • PID : unige:55426
Additional URL for this publicationhttp://cui.unige.ch/~dimarzo/papers/TR-98-265.pdf
520views
140downloads

Technical informations

Creation24/03/2015 18:35:00
First validation24/03/2015 18:35:00
Update time14/03/2023 23:10:18
Status update14/03/2023 23:10:18
Last indexation30/04/2025 15:17:34
All rights reserved by Archive ouverte UNIGE and the University of GenevaunigeBlack