en
Technical report
Open access
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
463views
126downloads

Technical informations

Creation03/24/2015 6:35:00 PM
First validation03/24/2015 6:35:00 PM
Update time03/14/2023 11:10:18 PM
Status update03/14/2023 11:10:18 PM
Last indexation05/02/2024 4:09:03 PM
All rights reserved by Archive ouverte UNIGE and the University of GenevaunigeBlack