论文部分内容阅读
本文提出在整个Java程序开发链中通过使用UML Statecharts对异常处理建模，对Statechart进行模型检验，完成代码生成。首先将Statecharts转换为EHA，然后给出其操作语义，根据操作语义映射到一个自动机。使用基于自动机理论的模型检验方法来验证基于EHA的异常处理模型是否满足某些关键性质，最后自动产生相关代码。