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.
Control software essentially consists of two functions:
1) ctrl_Law that chooses commands to be executed, and
2) ctrl_Region that checks if the current system state is in the domain of ctrl_Law.
Control software is traditionally designed using a separation-of-concerns approach.
Control Engineering techniques are used to design functional specification
from the closed loop system level functional specifications,
whereas Software Engineering techniques are used to
design control software implementing such specifications.
This approach has several drawbacks.
First, Control Engineering does not yield a formally verified specification
when quantization is taken into account.
This is the case when the plant has to be modelled as a Hybrid System,
that is a system with continuous as well as discrete state changes [AHH96].
As a result, even if the control software meets its functional
specifications there is no formal guarantee that system level specifications are met.
Second, non-functional requirements such as control software Worst Case Execution Time,
can only be considered only once the software has been designed.
This may trigger expensive software (or its functional specifications) redesign.
Finally, this approach does not support design space exploration.
Although there exists many functional specifications
for the control software, the software engineer only gets one to play with.
This overconstrains a priori the design space for the control software implementation
preventing, for example, effective performance trading.
More recently, abstraction based control synthesis
has become a fruitful research area [Tab09][MMST14].
Several control synthesis procedures has been devised [GPT10][LOTM13] for linear systems.
These works have been extended to the non-linear case [R11][G12][ZPMT12][AMSTT17].
Further techniques have been devised to make controllers guarantee some non-functional requirements
such as optimality with respect to some cost function [MT11][RR13][AMSST12a],
or controller robustness [LO14][GM12].
Our project aims to improve the state-of-the-art in this research line, by considering a new form
of system abstraction, namely history based abstraction.
History based controllers have been considered in Control Engineering [YBR+08], but not yet
int the context of correct-by-costruction controller synthesis.
By considering history based abstractions instead of just state abstraction,
we can reduce non-determinism of the system discrete abstraction.
Therefore, coarser abstractions involving only a subset of state variables could be enough.
The envisaged benefits of this approach are twofold.
1) synthesise controllers for systems whose state is only partially observable;
2) limit the state-explosion problem in the discrete abstraction, thus allowing to deal with larger systems than those considered so far.
[AHH96] R.Alur, T.A.Henzinger, P.-H.Ho.
Automatic symbolic verification of embedded systems.
IEEE TSE, 22(3):181¿201, 1996
[AMMST12a] V.Alimguzhin, F.Mari, I.Melatti, I.Salvo, E.Tronci.
Automatic control software synthesis for quantized discrete time hybrid systems.
In 51th CDC, p.6120¿6125. IEEE, 2012.
[AMMST17] V.Alimguzhin, F.Mari, I.Melatti, I.Salvo, E.Tronci.
Linearising Discrete Time Hybrid Systems.
IEEE TAC, 2017, to appear.
[G12] A.Girard.
Controller synthesis for safety and reachability via approximate bisimulation.
Automatica, 48(5):947¿953, 2012.
[GM12] A.Girard, S.Martin.
Synthesis for constrained nonlinear systems using hybridization and robust controllers on simplices. IEEE TAC, 57(4):1046¿1051, 2012.
[LOTM13] J.Liu, N.Ozay, U.Topcu, R.M.Murray.
Synthesis of reactive switching protocols from temporal logic specifications.
IEEE TAC, 58(7):1771¿1785, 2013.
[LO14] J.Liu, N.Ozay.
Abstraction, discretization, and robustness in temporal logic control of dynamical systems.
In 17th HSCC, p.293¿302. ACM, 2014.
[MMST14] F.Mari, I.Melatti, I.Salvo, E.Tronci.
Model based synthesis of control software from system level formal specifications.
ACM TOSEM, 23:Art. 6, 2014.
[MT11] M.Mazo, P. Tabuada.
Symbolic approximate time-optimal control.
Systems & Control Letters, 60(4):256¿263, 2011.
[R11] G.Reissig.
Computing abstractions of nonlinear systems.
IEEE TAC, 56(11):2583¿2598, 2011.
[RR13] G. Reissig, M.Rungger.
Abstraction-based solution of optimal stopping problems under uncertainty.
In 52nd CDC, p.3190¿3196, 2013.
[Tab09] Paulo Tabuada.
Verification and Control of Hybrid Systems: A Symbolic Approach.
Springer, 2009.
[YBR+08] V.Yousefzadeh, A.Babazadeh, B.Ramachandran, E.Alarcon, L.Pao, D.Maksimovic.
Approximate time-optimal digital control for synchronous buck dc¿dc converters.
IEEE Transactions on Power Electronics, 23(4):2018¿2026 (2008).
[ZPMT12]
M.Zamani, G.Pola, M.Mazo, and P.Tabuada.
Symbolic models for nonlinear control systems without stability assumptions.
IEEE TAC, 57(7):1804¿1809, 2012.