| Texto completo | |
| Autor(es): |
Hanazumi, Simone
;
de Melo, Ana C. V.
Número total de Autores: 2
|
| Tipo de documento: | Artigo Científico |
| Fonte: | JOURNAL OF SYSTEMS AND SOFTWARE; v. 131, p. 475-490, SEP 2017. |
| Citações Web of Science: | 0 |
| Resumo | |
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) | |
| Processo FAPESP: | 13/22317-6 - Geração de propriedades para o Java pathfinder a partir de objetivos de teste |
| Beneficiário: | Simone Hanazumi |
| Modalidade de apoio: | Bolsas no Exterior - Estágio de Pesquisa - Doutorado |
| Processo FAPESP: | 12/23767-2 - VVTransv: um método para teste e verificação formal transversal ao desenvolvimento de sistemas críticos |
| Beneficiário: | Ana Cristina Vieira de Melo |
| Modalidade de apoio: | Auxílio à Pesquisa - Regular |
| Processo FAPESP: | 11/01928-1 - Geração de Propriedades sobre Programas Java a partir de Objetivos de Teste |
| Beneficiário: | Simone Hanazumi |
| Modalidade de apoio: | Bolsas no Brasil - Doutorado |