Towards a Model-Based Framework for Automated Traceable Systems and Probabilistic Model Checking

The increasing complexity of modern software systems necessitates rigorous methods to verify non-functional requirements (NFRs) such as reliability, performance, and safety. Whilst probabilistic model checking (PMC) offers formal guarantees for systems with stochastic behaviors, its adoption remains challenging due to the expertise required in formal methods and the lack of traceability between evolving requirements and behavioral models. This paper presents MATS-PMC, a Model-based framework for Automated Traceable Systems and Probabilistic Model Checking, which integrates Model-Driven Engineering (MDE) with PMC to bridge the above gap. MATSPMC provides two synergistic environments: (1) a traceable model management environment for creating requirement models and bidirectional traceability links (in the form of traceability models), and (2) a probabilistic model management environment for synthesising probabilistic models and automating PRISM Language generation. The framework's effectiveness is demonstrated through an industrial Foreign Exchange (FX) trading case study, where system requirements are formally mapped to Markov models, enabling verification of probabilistic constraints (e.g., 0.92 success probability) and QoS metrics (e.g., cost-time tradeoffs). This work advances the practical adoption of formal methods by lowering the expertise barrier and providing essential traceability mechanisms critical for evolving systems.