| Summary: | This paper discusses the difficulty of transforming a trait-based model to a Markov Chain Model when the source model is a behavioral model. Therefore, we propose an innovative approach aimed at transforming trait-based models into Markov Chain Models. Our method hinges on the utilization of the Trait Component Ensemble Language (TCOEL) and the establishment of a unified model transformation specification at the meta-model level. Through this approach, we facilitate the seamless conversion of trait-based models into Markov Chain Models, thereby enhancing the adaptability and scope of the original models. The trait-based model presents quite challenging for transforming the behavioral traits directly into verification language. To overcome this difficulty, we analyzed the language behaviors using the fire brigade case study. Then, we used the description to identify and map the appropriate component in order to develop a CTMC model. Finally, we used PRISM model checker to undertake verification. © 2023 IEEE.
|
|---|