The digital revolution that we are witnessing stimulated the design of increasingly pervasive systems that are thought to control and coordinate various smart devices in order to manage assets and resources, and to guarantee efficient behaviours.
You may have heard of these systems as Cyber-Physical Systems. As the name suggests, they are characterised by a cybernetic component, which for simplicity we will henceforth call program, that has to operate in highly changing, physical conditions, henceforth referred to as the environment. Just to make a few examples, you can think of self-driven cars, industrial robotic systems, the heating system in a smart house, a drone that is autonomously setting its trajectory, etc.
Let us focus on the drone. Researchers carried out dozens of studies on how to synthesise a program to control the drone so that it can autonomously fly from a given point A to point B while avoiding the obstacles in between. The problem is that when we deploy the drone in the real world, it will also have to deal with a number of events that cannot be predicted at design time. For instance, a gust of wind may move the drone out its trajectory; there might be birds or other flying devices with which collisions must be prevented; a glass glare may alter some sensors measurements; the presence of wind can increase the battery consumption; etc.
So, what can we do to deal with this kind of unexpected, unpredictable, uncertain, events?
In this project we aim at developing a general framework for the modelling, analysis, and verification of systems in the presence of uncertainties.
Informally, we will develop formal tools that can be used to test the synthesised programs against the unpredictable environmental conditions before their deployment in the real world.