Enhancing Expressiveness in Stochastic Modelling of Cyber-Physical Systems

Cyber-physical systems (CPS) that exhibit stochastic behaviours and uncertainties can be modelled in various formalisms, that can be analysed and validated by model-checking tools. PRISM stands out as a robust probabilistic model checker but faces challenges in managing numerous models with diverse parameters, leading to redundancy and maintenance issues, or forcing part of the model to migrate into external scripts. To address this, we propose a novel extension to the PRISM language, enabling parameter specification within the language itself. This extension streamlines the modelling process, enhances efficiency, and mitigates maintenance complexities. We demonstrate the soundness of our extension and its effectiveness in generating multiple files for CPS-related case studies, offering a promising solution for improving stochastic modelling in PRISM.