Coordinating Exceptions of Java Systems: Implementation and Formal Verification

The exceptional behavior of software has become an important issue in software development since software may collapse if exception-handling is not implemented accordingly. Aiming at this problem, the Coordinated Atomic Action (CAA) model was proposed: it guides users to treat exceptions in a well-organized way, maintaining the whole system stable. However, deriving a system implementation from a CAA specification is not a straightforward task. This paper aims to provide a simple manner to implement reliable Java code using CAA concepts. To do this, a Java framework (in Java-SE) that implements a formal coordination model based on CAA is presented. In addition, we have defined, in Java Pathfinder (JPF) model checker, CAA properties regarding systems exceptional behavior. Then, using both the framework and JPF, software developers can quickly implement the systems coordination of exceptional behavior, via instantiation of the framework, and formally check the predefined exceptional behavior properties on code (using JPF).