[本文摘要]

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