基于动作序列的行为需求模式验证的研究

摘要：

提出了基于动作序列刻画安全关键系统的功能行为需求和安全性行为需求,较传统的类逻辑规范和类图式规范更准确表达交互行为间的时序关系.基于动作序列构造功能需求和安全需求两类行为模式,并给出每个模式的操作语义.为实现基于行为模式的需求验证,重新定义 LTS 安全性和活性的属性表达、组合操作,给出并证明功能需求模式和安全性需求模式满足的充要条件.该框架在高速铁路 CTCS2/3 的形式验证与确认得到了广泛应用,对指导构件化安全关键系统的组合形式验证具有较高的理论与实践价值.

关键词：安全关键系统、动作序列、行为需求模式、标签变迁系统、模式验证

所属期刊栏目：32

分类号：TP309(计算技术、计算机技术)

资助基金：国家自然科学基金资助项目60674004,60802042

在线出版日期：2011-05-30（万方平台首次上网日期，不代表论文的发表时间）

页数：共12页

页码：94-105