一种面向CPS的控制应用程序协同验证方法

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

作者：张雨,董云卫,冯文龙,黄梦醒

单位：张雨，南海海洋资源利用国家重点实验室(海南大学), 海南 海口 570228;海南大学 信息科学技术学院, 海南 海口 57022811,董云卫，西北工业大学 计算机学院, 陕西 西安 71012902,冯文龙，南海海洋资源利用国家重点实验室(海南大学), 海南 海口 570228;海南大学 信息科学技术学院, 海南 海口 57022803,黄梦醒，南海海洋资源利用国家重点实验室(海南大学), 海南 海口 570228;海南大学 信息科学技术学院, 海南 海口 57022804

摘要：信息-物理融合系统是一种新型嵌入式系统计算模式.它集成了控制计算过程和受控对象，二者相互影响并有机结合.随着信息技术在现实世界中更加广泛、深入的应用，智能化程度不断提升，在具有信息-物理紧密耦合特点的嵌入式系统中，嵌入式控制软件的功能比重急剧上升，作用更加突出.作为安全攸关的系统，需要引入形式化验证方法来保证嵌入式控制应用软件的安全性.基于自动机理论建立统一的系统验证模型，并针对系统的可达性、安全性（safety）和活性（liveness）等属性要求，提出了对该模型进行形式化验证的算法：基于有界模型检验方法，基于可达性将对系统模型的相关属性验证问题转换为可满足性判定问题.将活性转换为Büchi自动机，并基于四值语义进行判断.在求解过程中，通过偏序规约等手段化简了问题求解的规模，提高了可验证系统的规模.另外，结合协同仿真技术，灵活配置验证的场景，提高验证的可用性.实验结果表明，结合仿真，形式化协同验证方法可以有效地对系统进行验证.

关键词：信息-物理融合系统;嵌入式控制应用程序;自动机理论;协同验证;有界模型检验

基金资助：国家自然科学基金（61462022，61363071）；国家科技支撑计划（2014BAD10B04，2015BAH55F04）；海南省重大科技计划（ZDKJ2016015）；海南省自然科学基金（614232，614220）；海南省产学研一体化专项（cxy20150025）；海南大学科研启动基金（kyqd1610）