Verification of Exception Control Flows and Handlers Based on Architectural Scenarios

Brito, P.H.S. and de Lemos, R. and Rubira, C.M.F. (2008) Verification of Exception Control Flows and Handlers Based on Architectural Scenarios. In: 11th IEEE High Assurance Systems Engineering Symposium (HASE 2008), 3rd - 5th December, 2008, Nanjing, China. (The full text of this publication is not available from this repository)

The full text of this publication is not available from this repository. (Contact us about this Publication)
Official URL
http://dx.doi.org/10.1109/HASE.2008.11

Abstract

The use of exception handling mechanisms to develop robust software systems in a non-systematic manner can be a source of many design faults. This paper presents a rigorous development approach based on formal methods, which allows to systematise the verification of the system's abnormal behaviour at the architectural level. Our solution is based on the specification and verification of architectural scenarios, which describe both exception control flows and exception handlers involving architectural elements (components and connectors). We also adopt an architectural abstraction for guiding the internal structure of the architectural elements. The verification process is conducted using the ProB model checker, which combines the use of set-theory (B-Method) and a process algebra (CSP). The feasibility of our approach was evaluated by a case study from the financial domain.

Item Type: Conference or workshop item (Paper)
Uncontrolled keywords: Architectural exception handling , Formal verification of abnormal behaviour , Formal verification of software architectures , Software architecture
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Science Technology and Medical Studies > School of Computing
Depositing User: Rogerio de Lemos
Date Deposited: 05 Nov 2012 00:06
Last Modified: 21 Mar 2013 15:05
Resource URI: http://kar.kent.ac.uk/id/eprint/32080 (The current URI for this page, for reference purposes)
  • Depositors only (login required):