A Method for Model Checking Context-Aware Exception Handling

The context-aware exception handling (CAEH) is an error recovery technique employed to improve the ubiquitous software robustness. In the design of CAEH, context conditions are specified to characterize abnormal situations and used to select the proper handlers. The erroneous specification of such conditions represents a critical design fault that can lead the CAEH mechanism to behave erroneously or improperly at runtime (e.g., abnormal situations may not be recognized and the system´s reaction may deviate from what is expected). Thus, in order to improve the CAEH reliability this kind of design faults must be rigorously identified and eliminated from the design in the early stages of development. However, despite the existence of formal approaches to verify context-aware ubiquitous systems, such approaches lack specific support to verify the CAEH behavior. This work proposes a method for model checking CAEH. This method provides a set of modeling abstractions and 3 (three) properties formally defined that can be used to identify exiting design faults in the CAEH design. In order to assess the method feasibility: (i) a support tool was developed, and (ii) fault scenarios that are recurring in the CAEH was injected in a correct model and verified using the proposed approach.