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

发布时间：2018-09-18 14:09

【摘要】：信息-物理融合系统是一种新型嵌入式系统计算模式.它集成了控制计算过程和受控对象,二者相互影响并有机结合.随着信息技术在现实世界中更加广泛、深入的应用,智能化程度不断提升,在具有信息-物理紧密耦合特点的嵌入式系统中,嵌入式控制软件的功能比重急剧上升,作用更加突出.作为安全攸关的系统,需要引入形式化验证方法来保证嵌入式控制应用软件的安全性.基于自动机理论建立统一的系统验证模型,并针对系统的可达性、安全性(safety)和活性(liveness)等属性要求,提出了对该模型进行形式化验证的算法:基于有界模型检验方法,基于可达性将对系统模型的相关属性验证问题转换为可满足性判定问题.将活性转换为Büchi自动机,并基于四值语义进行判断.在求解过程中,通过偏序规约等手段化简了问题求解的规模,提高了可验证系统的规模.另外,结合协同仿真技术,灵活配置验证的场景,提高验证的可用性.实验结果表明,结合仿真,形式化协同验证方法可以有效地对系统进行验证.
[Abstract]:Information-physical fusion system is a new embedded system computing mode. It integrates the control computing process and the controlled object, and they interact with each other and combine organically. With the more extensive and in-depth application of information technology in the real world, the degree of intelligence has been improved continuously, and the function proportion of embedded control software has risen sharply in the embedded system with the characteristics of information and physical tight coupling. The role is more prominent. As a security related system, formal verification method should be introduced to ensure the security of embedded control applications. Based on the automata theory, a unified system verification model is established. According to the requirements of reachability, security (safety) and active (liveness), an algorithm for formal verification of the model is proposed: based on the bounded model checking method. Based on reachability, the problem of attribute verification for system model is transformed into satisfiability decision problem. The activity is converted to B 眉 chi automaton and judged on the basis of quaternary semantics. In the process of solving the problem, the scale of problem solving is simplified by means of partial order protocol, and the scale of verifiable system is improved. In addition, combined with collaborative simulation technology, the scenario of verification can be configured flexibly to improve the availability of verification. The experimental results show that the formal collaborative verification method can effectively validate the system.
【作者单位】：南海海洋资源利用国家重点实验室(海南大学);海南大学信息科学技术学院;西北工业大学计算机学院;
【基金】：国家自然科学基金(61462022,61363071) 国家科技支撑计划(2014BAD10B04,2015BAH55F04) 海南省重大科技计划(ZDKJ2016015) 海南省自然科学基金(614232,614220) 海南省产学研一体化专项(cxy20150025) 海南大学科研启动基金(kyqd1610)~~
【分类号】：TP311.1

【参考文献】