微型机与应用
微型機與應用
미형궤여응용
MICROCOMPUTER & ITS APPLICATIONS
2012年
8期
13-15
,共3页
反应系统%安全属性%UML状态空间图%相关事件集%状态转换
反應繫統%安全屬性%UML狀態空間圖%相關事件集%狀態轉換
반응계통%안전속성%UML상태공간도%상관사건집%상태전환
reactive systems%safety property%UML state space diagram%relevant event set%state transition
在总结前人工作的基础上,提出了一种有效检测并发或反应系统的动态行为模型中违反安全属性的方法,目的是减少为检测违反安全属性所需检测的状态数量,验证过程包括构造一个由所有独立状态图组成的全局状态空间图,并遍历这个全局状态空间图中的状态以便检测安全协议。首先读待验证的安全属性和可能会违反这些属性的相关事件集,构造全局状态空间图只考虑相关事件产生的状态转换。使用该方法验证了＂火车道口＂系统,减少了59%的搜索空间。
在總結前人工作的基礎上,提齣瞭一種有效檢測併髮或反應繫統的動態行為模型中違反安全屬性的方法,目的是減少為檢測違反安全屬性所需檢測的狀態數量,驗證過程包括構造一箇由所有獨立狀態圖組成的全跼狀態空間圖,併遍歷這箇全跼狀態空間圖中的狀態以便檢測安全協議。首先讀待驗證的安全屬性和可能會違反這些屬性的相關事件集,構造全跼狀態空間圖隻攷慮相關事件產生的狀態轉換。使用該方法驗證瞭＂火車道口＂繫統,減少瞭59%的搜索空間。
재총결전인공작적기출상,제출료일충유효검측병발혹반응계통적동태행위모형중위반안전속성적방법,목적시감소위검측위반안전속성소수검측적상태수량,험증과정포괄구조일개유소유독립상태도조성적전국상태공간도,병편력저개전국상태공간도중적상태이편검측안전협의。수선독대험증적안전속성화가능회위반저사속성적상관사건집,구조전국상태공간도지고필상관사건산생적상태전환。사용해방법험증료＂화차도구＂계통,감소료59%적수색공간。
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%。
