A Formal Approach to implement java exceptions in cooperative systems

Author(s)

Hanazumi, Simone ; de Melo, Ana C. V.

• Document type: Journal article
• Source: JOURNAL OF SYSTEMS AND SOFTWARE; v. 131, p. 475-490, SEP 2017.
• Web of Science Citations: 0

Abstract

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. (C) 2016 Elsevier Inc. All rights reserved. (AU)

• FAPESP's process: 13/22317-6 - Generation of Java pathfinder properties from test purposes
• Grantee: Simone Hanazumi
• Support Opportunities: Scholarships abroad - Research Internship - Doctorate
• FAPESP's process: 12/23767-2 - VVTransv: a method for traversing testing and verification through critical software development
• Grantee: Ana Cristina Vieira de Melo
• Support Opportunities: Regular Research Grants
• FAPESP's process: 11/01928-1 - Generation of Java Programs Properties from Test Purposes
• Grantee: Simone Hanazumi
• Support Opportunities: Scholarships in Brazil - Doctorate