Ricerc@Sapienza

Many Embedded Systems are indeed Software Based Control Systems (SBCSs).
A SBCS consists of two main subsystems: the controller and the plant.
Typically, the plant is a physical system whereas the controller consists
of control software running on a micro-controller.
The plant and the controller together form a closed-loop system.
Software generation from models and formal specifications is particularly interesting for SBCSs
in which system level specifications are much easier to define than the control software itself.
The long term goal is to generate correct-by-construction control software
from the plant model and formal specifications for the closed loop system behaviour.

Recently, in this context, abstraction based control synthesis has become a fruitful research area.
The idea is to build a finite discrete abstraction of the plant
and apply well-established control synthesis techniques for finite discrete systems.
Unfortunately, although several achievements have been carried out,
this approach hardly scales well with the complexity of the plant
and, so far, only systems whose state is described by up to 4 or 5 continuous variable can be handled
by using reasonable computational resources.

Our project aims to improve the state-of-the-art in this research field,
by considering a new form of system abstraction, namely history based abstraction.
The intuition is that considering system histories gives more information
than the observation of just system states.
Consequently, history based abstractions can reduce non-determinism of the system discrete
abstraction and therefore, coarser abstractions involving only a subset of state variables are enough.

The envisaged benefits of this approach are twofold.
1) synthesise controllers for systems whose state is only partially observable;
2) limit the state-explotion problem in the discrete abstraction,
thus allowing to deal with larger systems than those considered so far.