基于事件集的反应系统模型的验证

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