| Architecting Fault Tolerance with Exception Handling: Verification and Validation |
| |
| 作者姓名： | Rogério de Lemos Cecília M. F. Rubira |
| |
| 作者单位： | Institute;Computing;State;University;Campinas;Brazil;Laboratory;Kent;U.K.; |
| |
| 基金项目： | supported by Fapesp/Brazil under Grant No. 06/02116-2 and CAPES/Brazil under Grant No. 0722-07-3;;Cecília Rubira is partially supported by CNPq/Brazil under Grant Nos. 301446/2006-7 and 484138/2006-5 |
| |
| 摘 要： |
|
| 关 键 词： | |
Architecting Fault Tolerance with Exception Handling: Verification and Validation |
| |
| Patrick H. S. Brito,Rogério de Lemos,Cecília M. F. Rubira,Eliane Martins.Architecting Fault Tolerance with Exception Handling: Verification and Validation[J].Journal of Computer Science and Technology,2009,24(2):212-237. |
| |
| Authors: | Patrick H S Brito Rogério de Lemos Cecília M F Rubira Eliane Martins |
| |
| Affiliation: | (1) Institute of Computing, State University of Campinas, Campinas, Brazil;(2) Computing Laboratory, University of Kent, Kent, U.K. |
| |
| Abstract: | When building dependable systems by integrating untrusted software components that were not originally designed to interact
with each other, it is likely the occurrence of architectural mismatches related to assumptions in their failure behaviour.
These mismatches, if not prevented during system design, have to be tolerated during runtime. This paper presents an architectural
abstraction based on exception handling for structuring fault-tolerant software systems. This abstraction comprises several
components and connectors that promote an existing untrusted software element into an idealised fault-tolerant architectural
element. Moreover, it is considered in the context of a rigorous software development approach based on formal methods for
representing the structure and behaviour of the software architecture. The proposed approach relies on a formal specification
and verification for analysing exception propagation, and verifying important dependability properties, such as deadlock freedom,
and scenarios of architectural reconfiguration. The formal models are automatically generated using model transformation from
UML diagrams: component diagram representing the system structure, and sequence diagrams representing the system behaviour.
Finally, the formal models are also used for generating unit and integration test cases that are used for assessing the correctness
of the source code. The feasibility of the proposed architectural approach was evaluated on an embedded critical case study.
Patrick Brito is supported by Fapesp/Brazil under Grant No. 06/02116–2 and CAPES/Brazil under Grant No. 0722–07–3. Cecília
Rubira is partially supported by CNPq/Brazil under Grant Nos. 301446/2006–7 and 484138/2006–5. |
| |
| Keywords: | exception handling fault-tolerant software architecture model-based test model checking software verification and validation |
| 本文献已被 CNKI 万方数据 SpringerLink 等数据库收录！ |
|
|
下载PDF全文