西安电子科技大学学报（自然科学版）
西安電子科技大學學報（自然科學版）
서안전자과기대학학보（자연과학판）
JOURNAL OF XIDIAN UNIVERSITY(NATURAL SCIENCE)
2007年
5期
794-799
,共6页
模型检验%空属性探测%可计算时态逻辑公式%验证综合系统系统
模型檢驗%空屬性探測%可計算時態邏輯公式%驗證綜閤繫統繫統
모형검험%공속성탐측%가계산시태라집공식%험증종합계통계통
在模型检验中建立了一种新方法:检验可计算时态逻辑(CTL)公式描述的系统属性是否为空属性.根据原子命题的极性,用TRUE 或FALSE替换原子命题,得到一系列的CTL公式,再对这些CTL公式用模型检验工具验证,若CTL公式中有一个通过了验证,则可得出该系统属性是一个空属性.该方法对CTL公式的空属性的探测不需要对它的所有子公式用TRUE 或FALSE替换,只需对原子命题替换,这样检验的次数与原子命题的个数呈线性关系.利用验证综合系统对十字路口交通控制器规范的空属性进行了检验.
在模型檢驗中建立瞭一種新方法:檢驗可計算時態邏輯(CTL)公式描述的繫統屬性是否為空屬性.根據原子命題的極性,用TRUE 或FALSE替換原子命題,得到一繫列的CTL公式,再對這些CTL公式用模型檢驗工具驗證,若CTL公式中有一箇通過瞭驗證,則可得齣該繫統屬性是一箇空屬性.該方法對CTL公式的空屬性的探測不需要對它的所有子公式用TRUE 或FALSE替換,隻需對原子命題替換,這樣檢驗的次數與原子命題的箇數呈線性關繫.利用驗證綜閤繫統對十字路口交通控製器規範的空屬性進行瞭檢驗.
재모형검험중건립료일충신방법:검험가계산시태라집(CTL)공식묘술적계통속성시부위공속성.근거원자명제적겁성,용TRUE 혹FALSE체환원자명제,득도일계렬적CTL공식,재대저사CTL공식용모형검험공구험증,약CTL공식중유일개통과료험증,칙가득출해계통속성시일개공속성.해방법대CTL공식적공속성적탐측불수요대타적소유자공식용TRUE 혹FALSE체환,지수대원자명제체환,저양검험적차수여원자명제적개수정선성관계.이용험증종합계통대십자로구교통공제기규범적공속성진행료검험.
