| 基于事件集的反应系统模型的验证 |
| |
| 引用本文： | 张磊,马光胜.基于事件集的反应系统模型的验证[J].微型机与应用,2012,31(8):13-15. |
| |
| 作者姓名： | 张磊 马光胜 |
| |
| 作者单位： | 1. 黑龙江东方学院计算机科学与电气工程学部,黑龙江哈尔滨,150008
2. 哈尔滨工程大学计算机科学-9技术学院,黑龙江哈尔滨,150003 |
| |
| 摘 要： | 在总结前人工作的基础上,提出了一种有效检测并发或反应系统的动态行为模型中违反安全属性的方法,目的是减少为检测违反安全属性所需检测的状态数量,验证过程包括构造一个由所有独立状态图组成的全局状态空间图,并遍历这个全局状态空间图中的状态以便检测安全协议。首先读待验证的安全属性和可能会违反这些属性的相关事件集,构造全局状态空间图只考虑相关事件产生的状态转换。使用该方法验证了"火车道口"系统,减少了59%的搜索空间。
|
| 关 键 词： | 反应系统 安全属性 UML状态空间图 相关事件集 状态转换 |
Verification of model for reactive systems based-on event set |
| |
| Zhang Lei,Ma Guangsheng.Verification of model for reactive systems based-on event set[J].Microcomputer & its Applications,2012,31(8):13-15. |
| |
| Authors: | Zhang Lei Ma Guangsheng |
| |
| Affiliation: | 1.Institute of computer science and Electric Engineering,Heilongjiang East Academy,Harbin 150086,China;2.Department of Computer and Technology,Harbin Engineering University,Harbin 150001,China) |
| |
| Abstract: | A new method to detecting effectively safety violation in dynamic behavior model is proposed in this paper based on the study of predecessors’ work,which aim at reducing the number of states to be traversed for finding a property violation.The verification process involves building a global state space graph from these independent statechart.The authors applied the technology to the GRC(Generalized Railroad Crossing) systems and reduced space state by 59%。 |
| |
| Keywords: | reactive systems safety property UML state space diagram relevant event set state transition |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
