| UML Statecharts的切片模型检验方法 |
| |
| 作者姓名： | 董威 王戟 齐治昌 |
| |
| 作者单位： | 国防科技大学计算机学院, 湖南长沙, 410073 |
| |
| 基金项目： | 国家自然科学基金,国家高技术研究发展计划(863计划),教育部霍英东教育基金会高等院校青年教师基金,69973051,90104007,2001AA113202,,,, |
| |
| 摘 要： | 统一建模语言UML已被广泛应用于软件设计和开发中,而验证UML模型是否满足关键的性质需求成为一个重要问题.由于空间爆炸和语义的复杂性,对Statecharts进行模型检验受到软件规模和设计精化程度的制约.本文在用扩展层次自动机(EHA)结构化的表示UML Statecharts后,通过分析EHA中存在的层次、并发和事件同步等特征定义了一组依赖关系.对于由状态和迁移组成的切片准则,给出对EHA进行切片的算法.该算法能保证切片后的EHA与原来的Statecharts对性质具有相同的可满足性,且删除了与被验证性质无关的层次和并发状态,缓解了空间爆炸问题.
|
| 关 键 词： | UML Statecharts 模型检验 切片 |
| 文章编号： | 0372-2112(2002)12A-2082-07 |
| 收稿时间： | 2002-06-06 |
| 修稿时间： | 2002-06-06 |
| 本文献已被 万方数据 等数据库收录！ |
| 点击此处可从《电子学报》浏览原始摘要信息 |
|
点击此处可从《电子学报》下载全文 |
|
