微信服务号

微信订阅号

2025年4月1日 18:50 星期二
首页 > 过刊浏览>2017年第28卷第5期 >1144-1166. DOI:10.13328/j.cnki.jos.005214
PDF HTML阅读 XML下载 导出引用 引用提醒
一种面向CPS的控制应用程序协同验证方法
作者:
基金项目:

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


Co-Verification Approach to Control Software Program for CPS
Author:
Fund Project:

National Natural Science Foundation of China (61462022, 61363071); National Key Technology R&D Program of China (2014BAD10B04, 2015BAH55F04); Major Science and Technology Project of Hainan Province (ZDKJ2016015); Natural Science Foundation of Hainan Province (614232, 614220); Enterprises-Universities-Researches Integration Project of Hainan (cxy20150025); Scientific Research Staring Foundation of Hainan University (kyqd1610)

  • 摘要
    • | |
  • 访问统计
    • |
  • 参考文献 [29]
    • |
  • 相似文献 [20]
    • | | |
  • 文章评论
    摘要:

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

    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.

    参考文献
    [1] Lee EA. CPS foundations. In: Proc. of the 47th Design Automation Conf. (DAC). ACM, 2010. 737-742. [doi: 10.1145/1837274. 1837462]
    [2] Clarke E, Kroening D, Lerda F. A tool for checking ANSI-C programs. In: Jensen K, Podelski A, eds. Tools and Algorithms for the Construction and Analysis of Systems. LNCS 2988, Berlin, Heidelberg: Springer-Verlag, 2004. 168-176. [doi: 10.1007/978-3-540- 24730-2_15]
    [3] Beyer D, Keremoglu M, CPAchecker: A tool for configurable software verification. In: Gopalakrishnan G, Qadeer S, eds. Computer Aided Verification. LNCS 6806, Berlin, Heidelberg: Springer-Verlag, 2011. 184-190. [doi: 10.1007/978-3-642-22110- 1_16]
    [4] Ball T, Bounimova E, Kumar R, Levin V. SLAM2: Static driver verification with under 4% false alarms. In: Proc. of the 10th Int'l Conf. on Formal Methods in Computer-Aided Design, FMCAD 2010. Lugano, 2010. 35-42.
    [5] Henzinger T, Jhala R, Majumdar R, Sutre G. Software verification with BLAST. In: Model Checking Software. LNCS 2648, Berlin, Heidelberg: Springer-Verlag, 2003. 235-239. [doi: 10.1007/3-540-44829-2_17]
    [6] Havelund K, Pressburger T. Model checking Java programs using java pathfinder. Int'l Journal on Software Tools for Technology Transfer, 2000,2(4):366-381. [doi: 10.1007/s100090050043]
    [7] Holzmann G. The model checker spin. IEEE Trans. on Software Engineering, 1997,23(5):279-295. [doi: 10.1109/32.588521]
    [8] Herrmann P, Blech JO, Han FL, Schmidt H. A model-based toolchain to verify spatial behavior of cyber-physical systems. Int'l Journal of Web Services Research, 2016,13(1):40-52. [doi: 10.4018/IJWSR.2016010103]
    [9] Shan LJ, Zhou XS, Wang YY, Zhao L, Wan LJ, Qiao L, Chen JX. Statistical model checking of cyber-physical systems control software. Ruan Jian Xue Bao/Journal of Software, 2015,26(2):380-389 (in Chinese with English abstract). http//www.jos.org.cn/ 9825-1000/4788.html [doi: 10.13328/j.cnki.jos.004788]
    [10] Chan M, Ricketts D, Lerner S, Malecha G. Formal verification of stability properties of cyber-physical systems. 2016. http://www. chargueraud.org/events/coqpl2016/CoqPL_2016_paper_5.pdf
    [11] Bae K, Krisiloff J, Meseguer J, Ölveczky PC. Designing and verifying distributed cyber-physical systems using multirate PALS: An airplane turning control system case study. Science of Computer Programming, 2015,103:13-50. [doi: 10.1016/j.scico.2014.09. 011]
    [12] Majumdar R, Saha I. Symbolic robustness analysis. In: Proc. of the 30th IEEE of Real-Time Systems Symp (RTSS 2009). IEEE, 2009. 355-363. [doi: 10.1109/RTSS.2009.17]
    [13] Anta A, Majumdar R, Saha I, Tabuada P. Automatic verification of control system implementations. In: Proc. of the EMSOFT. 2010. [doi: 10.1145/1879021.1879024]
    [14] Majumdar R, Saha, Yazarel. Compositional equivalence checking for models and code of control systems. In: Proc. of 2013 IEEE the 52nd Annual Conf. on Decision and Control (CDC). 2013. 1564-1571. [doi: 10.1109/CDC.2013.6760105]
    [15] Lerda F, Kapinski J, Maka H, Clarke EM, Krogh BH. Model checking in-the-loop: Finding counterexamples by systematic simulation. In: Proc. of the American Control Conf. IEEE, 2008. 2734-2740. [doi: 10.1109/ACC.2008.4586906]
    [16] Pasareanu C, Schumann J, Mehlitz P, Lowry M, Karsai G, Nine H, Neema S. Model based analysis and test generation for flight software. In: Proc. of the 3rd IEEE Int'l Conf. on Space Mission Challenges for Information Technology (SMC-IT 2009). 2009. 83-90. [doi: 10.1109/SMC-IT.2009.18]
    [17] Bouissou O, Goubault E, Putot S, Tekkal K, Vedrine F. Hybridfluctuat: A static analyzer of numerical programs within a continuous environment. In: Bouajjani A, Maler O, eds Computer Aided Verification. LNCS 5643, Berlin, Heidelberg: Springer- Verlag, 2009. 620-626. [doi: 10.1007/978-3-642-02658-4_46]
    [18] Majumdar R, Saha I, Shashidhar K, Wang Z. CLSE: Closed-Loop symbolic execution. In: Goodloe A, Person S, eds. NASA Formal Methods. LNCS 7226, Berlin, Heidelberg: Springer-Verlag, 2012. 356-370. [doi: 10.1007/978-3-642-28891-3_33]
    [19] Zhang Y, Xie F, Dong YW, Zhou XS, Ma CY. Cyber/Physical co-verification for developing reliable cyber-physical systems. In: Proc. of 2013 IEEE the 37th Annual Computer Software and Applications Conf. IEEE Computer Society, 2013. 539-548. [doi: 10. 1109/COMPSAC.2013.88]
    [20] Biere A, Cimatti A, Clarke EM, Strichman O, Zhu YS. Bounded model checking. Advances in Computers, 2003,58(3):117-148. [doi: 10.1016/ S0065-2458(03)58003-2]
    [21] Pnueli A. The temporal logic of programs. In: Proc. of the 18th Annual Symp. on Foundations of Computer Science. 1977. 46-57. [doi: 10.1109/SFCS.1977.32]
    [22] Bauer A, Leucker M, Schallhart C. Comparing LTL semantics for runtime verification. Journal of Logic and Computation, 2010,20(3): 651-674. [doi: 10.1093/logcom/exn075]
    [23] Årźen K, Cervin A, Henriksson D. Implementation aware embedded control systems. In: Handbook of Networked and Embedded Control Systems. 2005. 377-394. [doi: 10.1007/0-8176-4404-0_16]
    [24] Schwoon S. Model-Checking pushdown systems [Ph.D. Thesis]. Technische Universität München, Institutfür Infomatik, 2002.
    [25] Henzinger TA. The theory of hybrid automata. In: Proc. of the Symp. on Logic in Computer Science. 1996. 278-292. [doi: 10.1109/ LICS.1996.561342]
    [26] Morse J, Cordeiro L, Nicole D, Fischer B. Model checking LTL properties over ANSI-C programs with bounded traces. Software & Systems Modeling, 2015,14:65-81. [doi: 10.1007/s10270-013-0366-0]
    [27] Zhang Y, Xie F, Dong YW, Yang G, Zhou XS. High fidelity virtualization of cyber-physical systems. Int'l Journal of Modeling, Simulation, and Scientific Computing, 2013,4(2):1340005. [doi: 10.1142/S1793962313400059]
    附中文参考文献:
    [9] 单黎君,周兴社,王宇英,赵雷,万丽景,乔磊,陈建新.信息物理融合系统控制软件的统计模型检验.软件学报,2015,26(2):380-389. http//www.jos.org.cn/9825-1000/4788.html [doi: 10.13328/j.cnki.jos.004788]
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

张雨,董云卫,冯文龙,黄梦醒.一种面向CPS的控制应用程序协同验证方法.软件学报,2017,28(5):1144-1166

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2016-07-15
  • 最后修改日期:2016-09-25
  • 在线发布日期: 2017-01-22
文章二维码
友情链接:中国科学院软件研究所中国计算机学会中国科学院国家自然科学基金委员会CCF数字图书馆Int'l J of Softw Info计算机系统应用
您是第19765662位访问者
版权所有：中国科学院软件研究所 京ICP备05046678号-3
地址：北京市海淀区中关村南四街4号,邮政编码：100190
电话：010-62562563 传真：010-62562533 Email：jos@iscas.ac.cn
技术支持：北京勤云科技发展有限公司

京公网安备 11040202500063号