A Formal Approach to implement java exceptions in cooperative systems

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.