A Formal Approach to implement java exceptions in cooperative systems

The CAA model coordinates recovering of cooperative systems exceptional behaviors.A Java framework that helps the implementation of CAA model is presented.CAA properties about system exceptional behavior were defined in JPF model checker.Using the framework we can write Java code following the CAA model in a simple way.Checking the CAA properties with JPF in that Java code can assure its correctness. The increasing number of systems that work on the top of cooperating elements have required new techniques to control cooperation on both normal and abnormal behaviors of systems. The controllability of the normal behaviors has received more attention because they are concerned with the users expectations, while for the abnormal behaviors it is left to designers and programmers. However, for cooperative systems, the abnormal behaviors, mostly represented by exceptions at programming level, become an important issue in software development because they can affect the overall system behavior. If an exception is raised and not handled accordingly, the system may collapse. To avoid such situation, certain concepts and models have been proposed to coordinate propagation and recovering of exceptional behaviors, including the Coordinated Atomic Actions (CAA). Regardless of the effort in creating these conceptual models, an actual implementation of them in real systems is not very straightforward.This article provides a reliable framework for the implementation of Java exceptions propagation and recovery using CAA concepts. To do this, a Java framework (based on a formal specification) is presented, together with a set of properties to be preserved and proved with the Java Pathfinder (JPF) model checker. In practice, to develop new systems based on the given coordination concepts, designers/programmers can instantiate the framework to implement the exceptional behavior and then verify the correctness of the resulting code using JPF. Therefore, by using the framework, designers/programmers can reuse the provided CAA implementation and instantiate fault-tolerant Java systems.