Statistical model checking of an energy-saving cyber-physical system in the railway domain

Studies devoted to reduce the energy consumption while guaranteeing acceptable reliability levels are nowadays gaining importance in a variety of application sectors. Analyses through formal models and tools help developers of energy supply strategies in properly trading between energy consumption and reliability. Generally, probabilistic phenomena are involved in those systems, and they can be modelled through stochastic formalisms. Validating these models is paramount, so to guarantee reliance on the analysis results they provide. In this paper, we uniformly address both evaluation and validation of energy consumption policies on a case study from the railway domain using formal techniques. In particular, we analyse a system of rail road switch heaters, which are used to keep the temperature of rail road switches above certain levels to assure their correct functioning. Strategies based on thresholds to control the energy supply are modelled through hybrid automata, a formalism which allows to analyse both the discrete and the continuous nature of cyber-physical systems. We verify the correctness of the proposed model, and we evaluate energy consumption and reliability indicators through Statistical Model Checking using the Uppaal SMC toolbox.