Contributo in atti di convegno, 2021, ENG, 10.1007/978-3-030-85248-1_3
ter Beek M.H.; Ciancia V.; Latella D.; Massink M.; Spagnolo G.O.
CNR-ISTI, Pisa, Italy; CNR-ISTI, Pisa, Italy; CNR-ISTI, Pisa, Italy; CNR-ISTI, Pisa, Italy; CNR-ISTI, Pisa, Italy
In this position paper, we discuss the introduction of spatial verification techniques in an application scenario from smart stations, viz. analysing the user experience with respect to the lighting conditions of station areas. This is a case study in industrial projects. We discuss three challenging use cases for the application of spatial model checking in this setting. First, we envision how to use the spatial model checker VoxLogicA, which can analyse both 2D and 3D voxel-based maps, to explore the areas that users can visit in a station area and to characterise them with respect to their illumination conditions. This is aimed at monitoring a smart station. We also ideate statistical spatio-temporal model checking of the design of energy-saving protocols, exploiting the modelling of user preferences. Finally, we discuss the idea of quantifying the impact of design changes, based on the logs of smart stations, to identify and measure the incidence of undesired events (e.g. non-illuminated platforms where a train is passing by) before and after each change.
FMICS 2021 - 26th International Conference on Formal Methods for Industrial Critical Systems, pp. 39–47, Online conference, 24-26/08/2021
Smart stations, Spatial logics, Spatial model checking, Spatio-temporal model checking
Massink Mieke, Ter Beek Maurice Henri, Latella Diego, Ciancia Vincenzo, Spagnolo Giorgio Oronzo
ISTI – Istituto di scienza e tecnologie dell'informazione "Alessandro Faedo"
ID: 455997
Year: 2021
Type: Contributo in atti di convegno
Creation: 2021-08-24 10:26:32.000
Last update: 2022-12-01 11:04:36.000
External links
OAI-PMH: Dublin Core
OAI-PMH: Mods
OAI-PMH: RDF
DOI: 10.1007/978-3-030-85248-1_3
URL: https://link.springer.com/chapter/10.1007/978-3-030-85248-1_3
External IDs
CNR OAI-PMH: oai:it.cnr:prodotti:455997
DOI: 10.1007/978-3-030-85248-1_3
Scopus: 2-s2.0-85115174104
ISI Web of Science (WOS): 000884726300003