通信学报

• • 上一篇    下一篇

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

杜军威,徐中伟,江 峰   

  • 出版日期:2011-01-25 发布日期:2011-01-15

  • Online:2011-01-25 Published:2011-01-15

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

[1] 赵慧玲,江志峰. 泛在传感器网络和业务[J]. 电信科学, 2009, 25(12): 1 -3 .
[2] 何业军,何 牧,朱光喜,刘德明. 基于最大似然估计的OFDM信号精确定位判决[J]. 通信学报, 2008, 29(11A): 14 -76 .
[3] 卢 力,王勇涛,田金文,柳 健. 基于SUSAN算法的遥感图像去云[J]. 通信学报, 2006, 27(8): 29 -164 .
[4] 杜结,沈成彬,蒋铭,王继东. 基于PON技术光接入网的运行、管理和维护[J]. 电信科学, 2010, 26(8): 24 -29 .
[5] 姚良,肖晴,施唯佳,奚溪. 智能电视终端的视频服务质量保障[J]. 电信科学, 2013, 29(4): 37 -40 .
[6] 张国梅,朱世华. 矢量正交频分复用系统的窄带干扰抑制[J]. 通信学报, 2008, 29(1): 1 -6 .
[7] 焦卫东,卢朝阳,何华君,郭大波. 基于Delaunay三角形网格的彩色视频帧间编码方法[J]. 通信学报, 2007, 28(9): 18 -124 .
[8] . 携手运营商聚焦新一代信息化[J]. 电信科学, 2011, 27(10): 131 -132 .
[9] 吴大鹏,楼芃雯,樊思龙,王汝言. 编码节点动态管理的间断连接无线网络数据转发机制[J]. 通信学报, 2014, 35(2): 4 -32 .
[10] 王艺. 云计算在物联网中的应用模式浅析[J]. 电信科学, 2011, 27(12): 26 -30 .