【摘要】 在总结前人工作的基础上,提出了一种有效检测并发或反应系统的动态行为模型中违反安全属性的方法,目的是减少为检测违反安全属性所需检测的状态数量,验证过程包括构造一个由所有独立状态图组成的全局状态空间图,并遍历这个全局状态空间图中的状态以便检测安全协议。首先读待验证的安全属性和可能会违反这些属性的相关事件集,构造全局状态空间图只考虑相关事件产生的状态转换。使用该方法验证了"火车道口"系统,减少了59%的搜索空间。更多还原

【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%。更多还原