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

来源：软件学报杂志2015年第2期北京时间：

作者：单黎君,周兴社,王宇英,赵雷,万丽景,乔磊,陈建新

单位：单黎君，西北工业大学 计算机学院, 陕西 西安 710072 ;国家数字交换系统工程技术研究中心, 河南 郑州 45000011,周兴社，西北工业大学 计算机学院, 陕西 西安 71007202,王宇英，西北工业大学 计算机学院, 陕西 西安 71007203,赵雷，北京控制工程研究所, 北京 10019004,万丽景，北京控制工程研究所, 北京 10019005,乔磊，北京控制工程研究所, 北京 10019006,陈建新，北京控制工程研究所, 北京 10019007

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

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

基金资助：国家自然科学基金(61472327)