主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2018-2019年专刊出版计划 微信服务介绍 最新一期:2018年第12期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
张雨,董云卫,冯文龙,黄梦醒.一种面向CPS的控制应用程序协同验证方法.软件学报,2017,28(5):1144-1166
一种面向CPS的控制应用程序协同验证方法
Co-Verification Approach to Control Software Program for CPS
投稿时间:2016-07-15  修订日期:2016-09-25
DOI:10.13328/j.cnki.jos.005214
中文关键词:  信息-物理融合系统  嵌入式控制应用程序  自动机理论  协同验证  有界模型检验
英文关键词:cyber-physical system  embedded control software program  automata theoretic  co-verification  bounded model checking
基金项目:国家自然科学基金(61462022,61363071);国家科技支撑计划(2014BAD10B04,2015BAH55F04);海南省重大科技计划(ZDKJ2016015);海南省自然科学基金(614232,614220);海南省产学研一体化专项(cxy20150025);海南大学科研启动基金(kyqd1610)
作者单位E-mail
张雨 南海海洋资源利用国家重点实验室(海南大学), 海南 海口 570228
海南大学 信息科学技术学院, 海南 海口 570228 
 
董云卫 西北工业大学 计算机学院, 陕西 西安 710129  
冯文龙 南海海洋资源利用国家重点实验室(海南大学), 海南 海口 570228
海南大学 信息科学技术学院, 海南 海口 570228 
 
黄梦醒 南海海洋资源利用国家重点实验室(海南大学), 海南 海口 570228
海南大学 信息科学技术学院, 海南 海口 570228 
huangmx09@163.com 
摘要点击次数: 1235
全文下载次数: 1127
中文摘要:
      信息-物理融合系统是一种新型嵌入式系统计算模式.它集成了控制计算过程和受控对象,二者相互影响并有机结合.随着信息技术在现实世界中更加广泛、深入的应用,智能化程度不断提升,在具有信息-物理紧密耦合特点的嵌入式系统中,嵌入式控制软件的功能比重急剧上升,作用更加突出.作为安全攸关的系统,需要引入形式化验证方法来保证嵌入式控制应用软件的安全性.基于自动机理论建立统一的系统验证模型,并针对系统的可达性、安全性(safety)和活性(liveness)等属性要求,提出了对该模型进行形式化验证的算法:基于有界模型检验方法,基于可达性将对系统模型的相关属性验证问题转换为可满足性判定问题.将活性转换为Büchi自动机,并基于四值语义进行判断.在求解过程中,通过偏序规约等手段化简了问题求解的规模,提高了可验证系统的规模.另外,结合协同仿真技术,灵活配置验证的场景,提高验证的可用性.实验结果表明,结合仿真,形式化协同验证方法可以有效地对系统进行验证.
英文摘要:
      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.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利