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

• 作者: 万丽景 乔磊 单黎君 周兴社 王宇英 赵雷 陈建新
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 形式化验证 统计模型检验 信息物理融合系统 多任务系统
• 年，卷（期）: 2015,（2）
• 页码范围: 380-389
• 页数: 10页
• 分类号: TP311
• 字数: 6015字
• 语种: 中文
• DOI: 10.13328/j.cnki.jos.004788

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	周兴社	西北工业大学计算机学院	251	2217	23.0	35.0
2	王宇英	西北工业大学计算机学院	13	83	6.0	8.0
3	乔磊		17	39	4.0	5.0
4	赵雷		5	41	4.0	5.0
5	陈建新		15	111	5.0	10.0
6	单黎君	西北工业大学计算机学院	1	6	1.0	1.0
10	万丽景		1	6	1.0	1.0