Verification of Exception Control Flows and Handlers Based on Architectural Scenarios

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.