微信服务号

微信订阅号

2025-4-15- 3
Home > Archive>Volume 32, Issue 6, 2021 >1779-1798. DOI:10.13328/j.cnki.jos.006249
PDF HTML XML Export Cite reminder
Hybrid AADL Modeling and Model Transformation for CPS Time and Space Properties Verification
Author:
Affiliation:

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)

  • Article
    • | |
  • Metrics
    • |
  • Reference [40]
    • |
  • Related
    • |
  • Cited by
    • | |
  • Comments
    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.

    Reference
    [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.
    Related
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

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

Copy
Share
Article Metrics
  • Abstract:1876
  • PDF: 5359
  • HTML: 3395
  • Cited by: 0
History
  • Received:August 30,2020
  • Revised:October 26,2020
  • Online: February 07,2021
  • Published: June 06,2021
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2035069Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address：4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code：100190
Phone：010-62562563 Fax：010-62562533 Email：jos@iscas.ac.cn
Technical Support：Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063