To go beyond, e.g. to prove robustness or stability, is is necessary to take into account the full feedback control system that is the controller (from which the control/command program was generated) but also the mathematical model of the physical system.
We advocate an approach in which code is generated by discretization both for the continuous dynamic nonlinear model of the controlled system (e.g. from the block diagram description of the plant, actuators and sensors) and for the digital implementation of the controller (as given by the control/command program to be verified) and then formally verified e.g. by reachability static analysis.
A central advantage of this integrated approach is the potential for early discovery of design errors much before the costly simulations and experimentations on an actual physical implementation. In particular backward analysis provide information not available by simulation.
\bibitem{Cousot05-APLAS}
P.~Cousot.
\newblock Integrating Physical Systems in the Static Analysis of
Embedded Control Software.
\newblock In \emph{Third Asian Symposium on Programming Languages
and Systems (APLAS'05)}, pages 135--138,
Tsukuba, Japan, November 3--5, 2005. Lecture Notes in Computer
Science, volume 3780, Springer, Berlin.
@inproceedings{Cousot05-APLAS,
author = {Cousot, P{.}},
title = {Integrating Physical Systems in the Static Analysis of
Embedded Control Software},
pages = {135--138},
booktitle = {Third Asian Symposium on Programming Languages
and Systems (APLAS'05)},
address = {Tsukuba, Japan, LNCS 3780},
publisher = {Springer, Berlin},
month = nov # " 3--5",
year = 2005,
}