西北工业大学学报
西北工業大學學報
서북공업대학학보
JOURNAL OF NORTHWESTERN POLYTECHNICAL UNIVERSITY
2005年
4期
516-519
,共4页
杨惠珍%康凤举%马裕民%蔡斌
楊惠珍%康鳳舉%馬裕民%蔡斌
양혜진%강봉거%마유민%채빈
时态逻辑%联邦%模型校核%形式化
時態邏輯%聯邦%模型校覈%形式化
시태라집%련방%모형교핵%형식화
提出了一种基于时态逻辑的形式化联邦校核方法,采用时态逻辑公式描述联邦各成员的行为逻辑关系,推导出与该时态逻辑公式对应的有限自动机模型,即规范自动机.同时,建立联邦全局行为的状态转移图,即实现自动机,通过检验规范自动机所接受的语言是否包含实现自动机所接受的语言来判断联邦运行时各成员的状态变化是否满足规范要求,达到校核联邦的目的.该方法可用来校核联邦及其成员的交互设计和逻辑行为运行的正确性和逻辑性,具有理论意义和应用价值.
提齣瞭一種基于時態邏輯的形式化聯邦校覈方法,採用時態邏輯公式描述聯邦各成員的行為邏輯關繫,推導齣與該時態邏輯公式對應的有限自動機模型,即規範自動機.同時,建立聯邦全跼行為的狀態轉移圖,即實現自動機,通過檢驗規範自動機所接受的語言是否包含實現自動機所接受的語言來判斷聯邦運行時各成員的狀態變化是否滿足規範要求,達到校覈聯邦的目的.該方法可用來校覈聯邦及其成員的交互設計和邏輯行為運行的正確性和邏輯性,具有理論意義和應用價值.
제출료일충기우시태라집적형식화련방교핵방법,채용시태라집공식묘술련방각성원적행위라집관계,추도출여해시태라집공식대응적유한자동궤모형,즉규범자동궤.동시,건립련방전국행위적상태전이도,즉실현자동궤,통과검험규범자동궤소접수적어언시부포함실현자동궤소접수적어언래판단련방운행시각성원적상태변화시부만족규범요구,체도교핵련방적목적.해방법가용래교핵련방급기성원적교호설계화라집행위운행적정학성화라집성,구유이론의의화응용개치.
