Verification of Ezception 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 systems 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.
Patrick H.S.Brito Rogerio de Lemos Cecilia M.F.Rubira
University of Campinas -UNICAMP, Brazil University of Kent, UK
国际会议
11th IEEE High Assurance Systems Engineering Symposium(HASE 2008)(第十一届IEEE高可信系统工程国际研讨会)
南京
英文
177-186
2008-12-03（万方平台首次上网日期，不代表论文的发表时间）