To validate the techniques, methodologies, and tools developed in the project we will consider three application scenarios that deal with smart systems of different scales:
These case studies are apt testbeds for the application and validation of the foundational theories, methods and tools developed in the project. All three call for runtime monitoring to control the interactions of the involved cyber-physical system. Moreover, smart transportation systems advocate the use of formal methods and model-checking tools to improve their scheduling and operation, next to safety and design time analysis. The enforcement of non-functional properties like energy efficiency and security are paramount for the success of smart city and housing systems.
The Centre for Urban Informatics and Modeling at the GSSI promotes and develops research and technology transfer projects, situated in the post-disaster context of the city of L’Aquila. The main focus of the centre is to make L’Aquila a “smart city”. One of the first core projects is devoted to “Environmental Monitoring”, with the aim of collecting and analyzing data to make informed decisions to improve the quality of life in the city. This involves the management of a large number of sensors, whose behaviour needs
These activities will be performed as part of this case study. Runtime monitoring for IoT systems is a challenging task for developers since the interaction among sensors, APIs and systems can be very complicated, and the amount of collected data can be huge.
The formal Methods and Tools group of the CNR has longstanding experience in the modelling and analysis of smart transportation systems, from bike-sharing to train-signalling systems. While satellite-based positioning systems have been in use for quite some time now in avionics and automotive sectors to provide accurate positioning and smart route planning, their application in the railway sector for moving block distancing and automatic driving is one of the current challenges of the EU H2020 Shift2Rail initiative. The railway sector’s robust safety requirements call for the use of state-of-the-art formal methods and tools for modelling and analysing technological advances during their development and for monitoring them at runtime.
The new Campus that is going be built at the University of Camerino after the 2016 earthquake will be integrated with a framework for “smart housing”. With smart housing we indicate a building that includes a system of devices that allow one to monitor and control activities and services. We will use the techniques developed in the project to develop a framework that, by integrating runtime monitoring techniques driven by the analyses performed at design time, allows for the enforcement of non-functional properties like efficiency (reduction of energy consumption) and security.