Istituto di Scienza e Tecnologie dell'Informazione     
Basile D., Di Giandomenico F., Gnesi S. Statistical model checking of an energy-saving cyber-physical system in the railway domain. In: SAC 2017 - 32th ACM SIGAPP Symposium on Applied Computing (Marrakesh, Marocco, 4-6 April 2017). Proceedings, pp. 1356 - 1363. ACM, 2017.
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.
URL: http://https://dl.acm.org/citation.cfm?doid=3019612.3019824
DOI: 10.1145/3019612.3019824
Subject Embedded and cyber-physical systems
Statistical Model Checking
D.2.4 SOFTWARE ENGINEERING. Software/Program Verification

Icona documento 1) Download Document PDF

Icona documento Open access Icona documento Restricted Icona documento Private


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional