An Automatic Transformation Method from AADL Reliability Model to CTMC
Cangzhou Yuan, Kangzhao Wu, Guotao Chen, Yongjia Mo · 2021
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.