微信服务号

微信订阅号

2025年3月24日 11:50 星期一
首页 > 过刊浏览>2021年第32卷第6期 >1779-1798. DOI:10.13328/j.cnki.jos.006249
PDF HTML阅读 XML下载 导出引用 引用提醒
面向CPS时空性质验证的混成AADL建模与模型转换方法
作者:
作者简介:

陈小颖(1997-),女,硕士,CCF学生会员,主要研究领域为软件工程,形式化方法,CPS系统.
赵宇(1997-),男,硕士,CCF学生会员,主要研究领域为软件工程,软件缺陷预测,机器学习.
祝义(1976-),男,博士,教授,CCF专业会员,主要研究领域为软件工程,形式化方法,CPS系统,智能软件开发.
王金永(1983-),男,博士生,CCF学生会员,主要研究领域为时空约束系统规约,协同无人驾驶安全性分析,形式化模型检测.

通讯作者:

祝义，zhuy@jsnu.edu.cn

基金项目:

国家自然科学基金（62077029）；徐州市应用基础研究计划（KC19004）；江苏省研究生科研创新计划（KYCX20_2380）；江苏省研究生科研创新计划（KYCX20_2384）


Hybrid AADL Modeling and Model Transformation for CPS Time and Space Properties Verification
Author:
Fund Project:

National Natural Science Foundation of China (62077029); Applied Basic Research Program of Xuzhou (KC19004); the Graduate Science Research Innovation Program of Jiangsu Province (KYCX20_2380); the Graduate Science Research Innovation Program of Jiangsu Province (KYCX20_2384)

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

    随着信息物理融合系统CPS （cyber physical system）研究的深入，CPS的安全性问题越来越受到人们的广泛关注，如何验证CPS时空不一致的安全性问题已经成为研究热点.针对该问题，提出了面向CPS时空性质验证的混成AADL（architecture analysis & design language）建模与模型转换方法.首先，扩展AADL行为附件的时空描述能力，提出了混成AADL（hybrid architecture analysis & design language），用于建模CPS的时空性质；其次，在进程代数中引入微分方程以及位置描述，提出了HP-TCSP，能够验证CPS的时空性质；再次，通过模型转换，将混成AADL转换为HP-TCSP，从而可以将混成AADL描述的CPS模型在HP-TCSP中进行时空一致性验证；最后，通过一个飞机避撞系统实例，验证该方法的有效性.

    Abstract:

    With the in-depth research of CPS (cyber physical system), the security problems of CPS are gradually attracted extensive attention. How to verify the security of space and time inconsistency of CPS has become a research hot spot. A hybrid AADL (architecture analysis & design language) modeling and model transformation method for CPS is proposed to solve this problem. Firstly, the time and space description capability of AADL behavior annex is extended, and Hybrid AADL (hybrid architecture analysis & design language) is proposed. Secondly, the differential equation and the position description are introduced into the process algebra. Thirdly, the hybrid AADL is transformed into HP-TCSP. Finally, the effectiveness of the proposed method is verified by an example of aircraft anti-collision system.

    参考文献
    [1] Zheng X, Julien C, Kim M, Khurshid S. Perceptions on the State of the art in verification and validation in cyber-physical systems. IEEE Systems Journal, 2017,11(4):2614-2627.
    [2] Banks VA, Plant KL, Stanton NA. Driver error or designer error:Using the perceptual cycle model to explore the circumstances surrounding the fatal tesla crash on 7th May 2016. Safety Science, 2018,108:278-285.
    [3] Feiler PH, Lewis B, Vestal S, Colbert E. An overview of the sae architecture analysis & design language (AADL) standard:A basis for model-based architecture-driven embedded systems engineering. Architecture Description Languages, 2005,176:3-15.
    [4] Zhang L. Specifying and modeling cloud cyber physical systems based on AADL. In:Proc. of the 17th Int'l Symp. on Distributed Computing and Appkications for Business Engineering and Science. Wuxi:Institute of Electrical and Electronics Engineers Inc, 2018. 26-29.
    [5] Goncalves FS, Pereira D, Tovar E, Becker LB. Formal verification of AADL models using UPPAAL. In:Proc. of the VII Brazilian Symp. on Computing Systems Engineering. Curitiba:IEEE Computer Society, 2017. 117-124.
    [6] Liu J, Li T, Ding Z. AADL+:A simulation-based methodology for cyber-physical systems. Frontiers of Computer Science, 2019, 13(3):516-538.
    [7] He R, Zhang W, Wu L. AADL-Based reliability modeling method of cyber-physical systems. In:Proc. of the WSSE2019. Wuhan:Association for Computing Machinery, 2019. 47-58.
    [8] Zhan H, Lin Q, Wang S. Unified graphical co-modelling of cyber-physical systems using AADL and simulink/stateflow. In:Ribeiro P, Sampaion A, eds. Proc. of the UTP 2019. Porto:Springer-Verlag, 2019. 109-129.
    [9] Dong YW, Wang GR, Zhang F, Gao L. AADL model reliability analysis and evaluation tool. Ruan Jian Xue Bao/Journal of Software, 2011,22(06):1252-1266(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/4014.htm[doi:10.3724/SP.J.1001.2011.04014]
    [10] Hoare CAR. Communicating sequential processes. Communications of the ACM, 1978,21(8):666-677
    [11] George M, Reed, Roscoe AW. A timed model for communicating sequential processes. In:Proc. of the 13th Int'l Colloquium on Automata, Languages and Programming (ICALP'86). Rennes, 1986.
    [12] Yang ZB, Hu K, Zhao YW, Ma DF, Jean-Paul BODEVEIX. Validation of AADL model based on time abstract state machine. Ruan Jian Xue Bao/Journal of Software, 2015,26(2):202-222(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/4776.htm[doi:10.13328/j.cnki.jos.004776]
    [13] Schneider S. An operational semantics for timed CPS. Information and Computation, 1995,116(2):193-213
    [14] Zhu Y, Huang ZQ, Cao ZN, Zhou H, Liu YP. A method of generating software architecture model based on formal specifications. Ruan Jian Xue Bao/Journal of Software, 2010,21(11):2738-2751(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/3701.htm[doi:10.3724/SP.J.1001.2010.03701]
    [15] Xu JM, Yang ZB, Huang ZQ, Xie J, Zhou Y. Functional behavior modeling extension of architecture analysis & design language (AADL). Computer Science and exploration, 2019,13(10):1638-1653(in Chinese with English abstract).
    [16] Li M, Zhuang Y, Hu TW. An embedded software reliability modeling and evaluation method combining AADL and Z. Computer Science, 2019,46(08):217-223(in Chinese with English abstract).
    [17] Cao XY, Cao ZN, Bu XC. Hybrid AADL modeling and model transformation for CPS. Computer Technology and Development, 2019,29(10):35-40(in Chinese with English abstract).
    [18] Bao YX, Chen MS, Zhu Q, Wei TQ, Frederic M, Zhou TL. Quantitative performance evaluation of uncertainty-aware hybrid AADL designs using statistical model checking. IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems, 2017, 36(12):1989-2002.
    [19] Liu X, Xie HM. AADL behavior model time consistency verification method. Computer Technology and Development, 2017, 27(7):1-5(in Chinese with English abstract).
    [20] Ahmad E, Dong YW, Larson B, Lü JD, Tang T, Zhan NJ. Behavior modeling and verification of movement authority scenario of Chinese train control system using AADL. Science China (Information Sciences), 2015,58(11):125-144.
    [21] Hou G. Modeling, verification and analysis of cyber physical system software[Ph.D. Thesis]. Dalian:Dalian University of Technology, 2018(in Chinese with English abstract).
    [22] Luo CX, Wang R, Guan Y, Li XJ, Shi ZP, Song XY. CPS integrated modeling method for real-time data. Ruan Jian Xue Bao/Journal of Software, 2019,30(7):1966-1979(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/30/1966.htm
    [23] Ye F, Xia Y, Shen ZX, Zhu YC. CPS modeling method based on dynamic behavior modeling. Journal of System Simulation, 2016, 28(05):1003-1008,1016(in Chinese with English abstract).
    [24] Zhang ZH, Zhu Y, Xiao FX. Modelling and analysis of real-time and reliability for WSN-based CPS. Int'l Journal of Internet Protocol Technology (IJIPT), 2019,12(2).
    [25] Su Q, Wang T, Chen TM, Chen RR. CPS security modeling and validation based on time automaton. Information Security Research, 2017,3(7):601-609(in Chinese with English abstract).
    [26] Zhang J, Wang L, Fan HB. Modeling and analysis of CPS physical entity spatio-temporal state. Computer Engineering and Applications, 2018,54(14):41-44(in Chinese with English abstract).
    [27] Zhao HZ, Cheng S, Yue H. Using CSTPNs to model traffic control CPS. IET Software, 2017,11(3):116-125.
    附中文参考文献:
    [9] 董云卫,王广仁,张凡,高磊.AADL模型可靠性分析评估工具.软件学报,2011,22(6):1252-1266. http://www.jos.org.cn/1000-9825/4014.htm[doi:10.3724/SP.J.1001.2011.04014]
    [12] 杨志斌,胡凯,赵永望,马殿富,Jean-Paul BODEVEIX.基于时间抽象状态机的AADL模型验证.软件学报,2015,26(2):202-222. http://www.jos.org.cn/1000-9825/4776.htm[doi:10.13328/j.cnki.jos.004776]
    [14] 祝义,黄志球,曹子宁,周航,刘亚萍.一种基于形式化规约生成软件体系结构模型的方法.软件学报,2010,21(11):2738-2751. http://www.jos.org.cn/1000-9825/3701.htm[doi:10.3724/SP.J.1001.2010.03701]
    [15] 许金淼,杨志斌,黄志球,谢健,周勇.系统架构描述语言AADL的功能行为建模扩展.计算机科学与探索,2019,13(10):1638-1653.
    [16] 李蜜,庄毅,胡镡文.一种结合AADL与Z的嵌入式软件可靠性建模与评估方法.计算机科学,2019,46(8):217-223.
    [17] 曹雪岳,曹子宁,卜星晨.面向CPS的混成AADL建模与模型转换.计算机技术与发展,2019,29(10):35-40.
    [19] 刘骁,谢红梅.AADL行为模型时间一致性验证方法.计算机技术与发展,2017,27(7):1-5.
    [21] 侯刚.信息物理系统软件的形式建模、验证与分析[博士学位论文].大连:大连理工大学,2018.
    [22] 罗晨霞,王瑞,关永,李晓娟,施智平,SONG XY.面向实时数据的CPS一体化建模方法.软件学报,2019,30(7):1966-1979. http://www.jos.org.cn/1000-9825/5753.htm[doi:10.13328/j.cnki.jos.005753]
    [23] 叶枫,夏阳,申朝祥,朱云超.基于动态行为建模的CPS计算实体建模方法.系统仿真学报,2016,28(5):1003-1008,1016.
    [25] 苏琪,王婷,陈铁明,陈蓉蓉.基于时间自动机的CPS安全建模和验证.信息安全研究,2017,3(7):601-609.
    [26] 张晶,王亮,范洪博.CPS系统物理实体时空一致性建模与分析.计算机工程与应用,2018,54(14):41-44.
    相似文献
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

陈小颖,祝义,赵宇,王金永.面向CPS时空性质验证的混成AADL建模与模型转换方法.软件学报,2021,32(6):1779-1798

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

京公网安备 11040202500063号