@inproceedings{512da11c31954aa791b4e8ceceb1ddaf,
title = "An automatic transformation method from AADL reliability model to CTMC",
abstract = "AADL is a semi-formal architecture modeling language for the embedded field. Continuous Time Markov Chain (CTMC) is a formal model for reliability evaluation. In the process of quantitatively evaluating the reliability of embedded software, the AADL model needs to be transformed to the CTMC model, but the semantic gap between AADL and CTMC is too large to be directly transformed. This paper proposes a transformation method, which transforms AADL into PRISM- CTMC, a CTMC model described in PRISM language. This method uses PRISM as an intermediate language to reduce the difficulty of transformation between AADL and CTMC. This paper implements a transformation tool based on this method and evaluates the reliability of the flight control system (FCS) with the aid of the PRISM model checking tool, which verifies the effectiveness of the transformation method.",
keywords = "AADL, CTMC, Model transformation, PRISM, Reliability",
author = "Cangzhou Yuan and Kangzhao Wu and Guotao Chen and Yongjia Mo",
note = "Publisher Copyright: {\textcopyright} 2021 IEEE.; 2021 IEEE International Conference on Information Communication and Software Engineering, ICICSE 2021 ; Conference date: 19-03-2021 Through 21-03-2021",
year = "2021",
month = mar,
day = "19",
doi = "10.1109/ICICSE52190.2021.9404135",
language = "英语",
series = "2021 IEEE International Conference on Information Communication and Software Engineering, ICICSE 2021",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
pages = "322--326",
booktitle = "2021 IEEE International Conference on Information Communication and Software Engineering, ICICSE 2021",
address = "美国",
}