Page 223 - 《软件学报》2021年第6期

陈小颖 等:面向 CPS 时空性质验证的混成 AADL 建模与模型转换方法 1797

References:
[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).