信息物理融合系统控制软件的统计模型检验

被引：6

作者：

单黎君 ^{[1
,2
]}

周兴社 ^{[1
]}

王宇英 ^{[1
]}

赵雷 ^{[3
]}

万丽景 ^{[3
]}

乔磊 ^{[3
]}

陈建新 ^{[3
]}

机构：

[1] 西北工业大学计算机学院

[2] 国家数字交换系统工程技术研究中心

[3] 北京控制工程研究所

来源：

软件学报 | 2015年 / 26卷 / 02期

关键词：

形式化验证; 统计模型检验; 信息物理融合系统; 多任务系统;

D O I：

暂无

中图分类号：

TP202 [设计、性能分析与综合]; TP311.52 [];

学科分类号：

140102 [集成电路设计与设计自动化];

摘要：

信息物理融合系统常采用嵌入式实时多任务系统作为其控制软件,这类软件的并发和非确定性给验证带来了困难.提出了一种利用统计模型检验技术分析多任务系统的功能正确性的方法.该方法构造的时间自动机模型以模块化的方式描述了实时多任务系统中的主要成分,包括实时操作系统、周期性任务、偶发任务、共享资源以及物理环境,能够展现多任务系统的细粒度的运行过程及其对物理环境的实时响应.应用该方法分析了玉兔号月球车控制软件的一个早期版本,发现了系统运行中出现的一个特殊错误,识别了实际系统出现错误的条件,再现了出现错误的场景.

引用

页码：380 / 389

页数：10