In: Proc. 5th Int. Conf. on Engineering of Complex Computer Systems, 18-21 October 1999, Las Vegas, NV, pages 98-108. 1999. URL: http://cui.unige.ch/~dimarzo/papers/iceccs99.pdf.
Abstract: The rapid expansion of Java programs into software market is often not supported by a proper 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 with respect to 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 upon implementation constraints and provides a centralized solution; second, dependability and distribution constraints are integrated; third, the Java implementation is performed. The CO-OPN/2 specification language which integrates Petri nets and algebraic specifications, is used to express specifications formally, and the dependability and distributed 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: CA actions, CO-OPN/2, Java, Petri nets, algebraic specifications, dependable systems, design for validation, distributed applications, formal development, formal validation, specification languages, stepwise refinements.