计算机应用研究
計算機應用研究
계산궤응용연구
APPLICATION RESEARCH OF COMPUTERS
2015年
5期
1486-1488
,共3页
赵梦龙%唐郑熠%万良%韦立
趙夢龍%唐鄭熠%萬良%韋立
조몽룡%당정습%만량%위립
互斥协议%属性分类%安全性%活性%行为时序逻辑
互斥協議%屬性分類%安全性%活性%行為時序邏輯
호척협의%속성분류%안전성%활성%행위시서라집
mutual exclusion protocol%classification of properties%safety%liveness%temporal logic of action
安全性和活性是两大基本的系统属性,对于指导系统的设计与验证具有重要意义。通过对它们原始定义的形式化梳理,发现其缺乏对状态序列的具体约束。针对这一问题,使用对系统动作刻画更完善的行为时序逻辑进行了重定义,加入了初始状态和转移条件的约束。以此为基础,对互斥这一并发系统的典型属性进行了形式化的分析,由此说明如何判断一个属性是否满足安全性或活性的定义。该技术为实现系统性质的自动推理与验证提供了形式化基础。
安全性和活性是兩大基本的繫統屬性,對于指導繫統的設計與驗證具有重要意義。通過對它們原始定義的形式化梳理,髮現其缺乏對狀態序列的具體約束。針對這一問題,使用對繫統動作刻畫更完善的行為時序邏輯進行瞭重定義,加入瞭初始狀態和轉移條件的約束。以此為基礎,對互斥這一併髮繫統的典型屬性進行瞭形式化的分析,由此說明如何判斷一箇屬性是否滿足安全性或活性的定義。該技術為實現繫統性質的自動推理與驗證提供瞭形式化基礎。
안전성화활성시량대기본적계통속성,대우지도계통적설계여험증구유중요의의。통과대타문원시정의적형식화소리,발현기결핍대상태서렬적구체약속。침대저일문제,사용대계통동작각화경완선적행위시서라집진행료중정의,가입료초시상태화전이조건적약속。이차위기출,대호척저일병발계통적전형속성진행료형식화적분석,유차설명여하판단일개속성시부만족안전성혹활성적정의。해기술위실현계통성질적자동추리여험증제공료형식화기출。
Safety and liveness are tow basic types of system property and are very useful for the design and verification of sys-tem.This paper pointed out the disadvantage of lacking restricts to state sequence in their original definition.For this prob-lem, it gave redefinition by the temporal logic of action which was more suitable to describe system action.The new formal def-inition added initial state and constraint conditions for transfer.On this basis, it analyzed the mutual exclusion which was the typical property of concurrent system by formal method.It also shows that how to judge whether a property meets the definition of safety or liveness.This technology provided the formal basic for the automatic reasoning and verification of system property.