| 本文已被：浏览 5104次 下载 9745次 |
码上扫一扫！ |
|
|
| 一种面向CPS的控制应用程序协同验证方法 |
|
张雨1,2, 董云卫3, 冯文龙1,2, 黄梦醒1,2
|
|
1.南海海洋资源利用国家重点实验室(海南大学), 海南 海口 570228;2.海南大学 信息科学技术学院, 海南 海口 570228;3.西北工业大学 计算机学院, 陕西 西安 710129
|
|
| 摘要: |
| 信息-物理融合系统是一种新型嵌入式系统计算模式.它集成了控制计算过程和受控对象，二者相互影响并有机结合.随着信息技术在现实世界中更加广泛、深入的应用，智能化程度不断提升，在具有信息-物理紧密耦合特点的嵌入式系统中，嵌入式控制软件的功能比重急剧上升，作用更加突出.作为安全攸关的系统，需要引入形式化验证方法来保证嵌入式控制应用软件的安全性.基于自动机理论建立统一的系统验证模型，并针对系统的可达性、安全性（safety）和活性（liveness）等属性要求，提出了对该模型进行形式化验证的算法：基于有界模型检验方法，基于可达性将对系统模型的相关属性验证问题转换为可满足性判定问题.将活性转换为Büchi自动机，并基于四值语义进行判断.在求解过程中，通过偏序规约等手段化简了问题求解的规模，提高了可验证系统的规模.另外，结合协同仿真技术，灵活配置验证的场景，提高验证的可用性.实验结果表明，结合仿真，形式化协同验证方法可以有效地对系统进行验证. |
| 关键词: 信息-物理融合系统 嵌入式控制应用程序 自动机理论 协同验证 有界模型检验 |
| DOI：10.13328/j.cnki.jos.005214 |
| 分类号: |
| 基金项目:国家自然科学基金（61462022，61363071）；国家科技支撑计划（2014BAD10B04，2015BAH55F04）；海南省重大科技计划（ZDKJ2016015）；海南省自然科学基金（614232，614220）；海南省产学研一体化专项（cxy20150025）；海南大学科研启动基金（kyqd1610） |
|
| Co-Verification Approach to Control Software Program for CPS |
|
ZHANG Yu1,2, DONG Yun-Wei3, FENG Wen-Long1,2, HUANG Meng-Xing1,2
|
|
1.State Key Laboratory of Marine Resource Utilization in South China Sea (Hainan University), Haikou 570228, China;2.College of Information Science and Technology, Hainan University, Haikou 570228, China;3.School of Computer Science, Northwestern Polytechnical University, Xi’an 710129, China
|
| Abstract: |
| Cyber-Physical System (CPS) tightly integrates control software and embedded components, incorporating software with control domains. CPSs are pervasive and often mission-critical, therefore, they must have high level of security. With the extensive use of information technology, embedded control software plays a greater role in such systems. The close interactions between control software and embedded components demand co-verification. In this paper, an automata-theoretic approach is presented to co-verification. Co-verification, which verifies control software and embedded components together, is essential to establish the correctness of a complete system. The foundation of this approach is a unified model for co-verification and reachability analysis of the model. The LTL formula is converted into a Büchi automata, which is interleaved with the execution of the unified model under analysis. An online-capture offline-replay approach is proposed to improve the usefulness for formal verification. Case studies on a suite of realistic examples show that the presented approach has major potential in verifying system level properties, therefore improving the high-assurance of system. |
| Key words: cyber-physical system embedded control software program automata theoretic co-verification bounded model checking |
