通信学报
通信學報
통신학보
JOURNAL OF CHINA INSTITUTE OF COMMUNICATIONS
2011年
1期
94-105
,共12页
安全关键系统%动作序列%行为需求模式%标签变迁系统%模式验证
安全關鍵繫統%動作序列%行為需求模式%標籤變遷繫統%模式驗證
안전관건계통%동작서렬%행위수구모식%표첨변천계통%모식험증
提出了基于动作序列刻画安全关键系统的功能行为需求和安全性行为需求,较传统的类逻辑规范和类图式规范更准确表达交互行为间的时序关系.基于动作序列构造功能需求和安全需求两类行为模式,并给出每个模式的操作语义.为实现基于行为模式的需求验证,重新定义 LTS 安全性和活性的属性表达、组合操作,给出并证明功能需求模式和安全性需求模式满足的充要条件.该框架在高速铁路 CTCS2/3 的形式验证与确认得到了广泛应用,对指导构件化安全关键系统的组合形式验证具有较高的理论与实践价值.
提齣瞭基于動作序列刻畫安全關鍵繫統的功能行為需求和安全性行為需求,較傳統的類邏輯規範和類圖式規範更準確錶達交互行為間的時序關繫.基于動作序列構造功能需求和安全需求兩類行為模式,併給齣每箇模式的操作語義.為實現基于行為模式的需求驗證,重新定義 LTS 安全性和活性的屬性錶達、組閤操作,給齣併證明功能需求模式和安全性需求模式滿足的充要條件.該框架在高速鐵路 CTCS2/3 的形式驗證與確認得到瞭廣汎應用,對指導構件化安全關鍵繫統的組閤形式驗證具有較高的理論與實踐價值.
제출료기우동작서렬각화안전관건계통적공능행위수구화안전성행위수구,교전통적류라집규범화류도식규범경준학표체교호행위간적시서관계.기우동작서렬구조공능수구화안전수구량류행위모식,병급출매개모식적조작어의.위실현기우행위모식적수구험증,중신정의 LTS 안전성화활성적속성표체、조합조작,급출병증명공능수구모식화안전성수구모식만족적충요조건.해광가재고속철로 CTCS2/3 적형식험증여학인득도료엄범응용,대지도구건화안전관건계통적조합형식험증구유교고적이론여실천개치.
