Approach of Model Checking for Exception Handling Based on EHA
基于EHA的异常处理模型检验方法

This paper proposes an approach of handling exception throughout the entire development chain of Java programs by modeling exception handling in the UML statechart model, then model checking statecharts and utilizing automatic code generators for implementing the source. At first, the system statecharts model is converted into automaton by EHA operational semantics. The statecharts model is verified whether satisfies the some key properties.Lastly, source code are generated.