|
|||||
|
|
| 基于EHA的异常处理模型检验方法 | |
| 引用本文： | 杨厚群,何中市,陈静. 基于EHA的异常处理模型检验方法[J]. 计算机科学, 2008, 35(4): 280-282 |
| 作者姓名： | 杨厚群 何中市 陈静 |
| 作者单位： | 1. 重庆大学计算机学院,重庆,400044;海南大学信息科学技术学院,海口,570228 2. 重庆大学计算机学院,重庆,400044 3. 海南大学信息科学技术学院,海口,570228 |
| 基金项目： | 海南省教育厅高校科研项目 |
| 摘 要： | 本文提出在整个Java程序开发链中通过使用UML Statecharts对异常处理建模,对Statechart进行模型检验,完成代码生成.首先将Statecharts转换为EHA,然后给出其操作语义,根据操作语义映射到一个自动机.使用基于自动机理论的模型检验方法来验证基于EHA的异常处理模型是否满足某些关键性质,最后自动产生相关代码. |
| 关 键 词： | 异常处理 模型检验 EHA |
Approach of Model Checking for Exception Handling Based on EHA |
|
| YANG Hou-Qun,HE Zhong-Shi,CHEN Jing. Approach of Model Checking for Exception Handling Based on EHA[J]. Computer Science, 2008, 35(4): 280-282 | |
| Authors: | YANG Hou-Qun HE Zhong-Shi CHEN Jing |
| Affiliation: | YANG Hou-Qun1,2 HE Zhong-Shi1 CHEN Jing2(College of Computer Science,Chongqing University,Chongqing 400044)1 (College of Information Science & Technology,Hainan University,Haikou 570228)2 |
| Abstract: | 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. |
| Keywords: | Exception handling Model checking EHA |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ | |
| 点击此处可从《计算机科学》下载全文 | |