A Formal Approach to implement java exceptions in cooperative systems

作者：Hanazumi Simone; de Melo Ana C V^*

来源：Journal of Systems and Software, 2017, 131: 475-490.

DOI：10.1016/j.jss.2016.07.033

• Coordinated atomic actions model
• concurrent exception handling
• java framework
• program verification

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.

• 出版日期2017-9