Research on verification of behavior requirement patterns based on action sequences

DU Jun-wei1; XU Zhong-wei2; JIANG Feng1

您当前的位置：

首页 >

文章列表页 >

Research on verification of behavior requirement patterns based on action sequences

更新时间：2024-10-14

- Research on verification of behavior requirement patterns based on action sequences
- Vol. 32, Issue 1, Pages: 94-105(2011)
- 作者机构：
  
  1. 青岛科技大学信息科学技术学院
  2. 同济大学电子与信息工程学院
- 作者简介：
- 基金信息：
- DOI：
  CLC： TP309
- Published：2011
- 稿件说明：
移动端阅览
DU Jun-wei1, XU Zhong-wei2, JIANG Feng1. Research on verification of behavior requirement patterns based on action sequences[J]. 2011, 32(1): 94-105.
DOI：

DU Jun-wei1, XU Zhong-wei2, JIANG Feng1. Research on verification of behavior requirement patterns based on action sequences[J]. 2011, 32(1): 94-105. DOI：

摘要

提出了基于动作序列刻画安全关键系统的功能行为需求和安全性行为需求

较传统的类逻辑规范和类图式规范更准确表达交互行为间的时序关系。基于动作序列构造功能需求和安全需求两类行为模式

并给出每个模式的操作语义。为实现基于行为模式的需求验证

重新定义LTS安全性和活性的属性表达、组合操作

给出并证明功能需求模式和安全性需求模式满足的充要条件。该框架在高速铁路CTCS2/3的形式验证与确认得到了广泛应用

对指导构件化安全关键系统的组合形式验证具有较高的理论与实践价值。

Abstract

Function behavior requirements（FBR） and safety behavior requirements（SBR） were described by action se-quences.Compared with the traditional logic or graphic form

action sequences can express the temporal relationship among interactive behaviors more exactly.Moreover

FBR pattern and SBR pattern are constructed by action sequences

and the operation semantics of these patterns are also given.To implement the requirement verification based on behavior patterns

the necessary and sufficient conditions as well as the checking algorithm for the satisfiability of FBR pattern and SBR pattern are presented and proven by redefining the property expression and combination operation of LTS’s safety and liveness.The framework has been widely applied in the formal verification ＆ validation of component-based CTCS2/3 systems

and has shown great theoretical and practical significance to combinational verification of Compo-nent-based safety-critical systems.

关键词

Keywords

references

Views

755

下载量

CSCD

Alert me when the article has been cited

提交

Tools

Publicity Resources

Research on safety methods of airborne embedded software

Related Author

Ya-hui LI

Ya-di ZHANG

Peng GUO

Related Institution

Airborne and Missile-borne Computer Aviation technology Key Lab,Aeronautical Computing Technique Research Institute

AI问答

⁰