Abstract:
The design of hardware and software for safety critical applications often involves
use of formal veri cation techniques to ensure correctness of implementation. If
speci cation fails to satisfy then the cycle of design and veri cation needs to be
repeated. Lengthy and costly design process can be avoided by the use of automated
controller synthesis techniques which can provide correct-by-construction
controller that enforces the desired formal speci cation on the given system. Use
of synthesis techniques with continuous systems require construction of a symbolic
model which in turn require computation of reachable sets. The set of states that
can be attained by a system for given values of initial state, input and time horizon
is referred to as reachable state set.
As reachable sets are in nite objects their exact computation is di cult, thus their
overapproximations are usually computed whose accuracy a ects the computation
time and size of the synthesized controller. The choice of set representation also
plays an important role in accuracy of approximation and time requirement. We
used zonotopes which are centrally symmetric convex polytopes and are closed
under linear transformation and Minkowski sum.
After a short introduction to the process of symbolic model construction we discuss
three methods of reachable set computation for nonlinear control systems.
These are then used together with SCOTS, which is a tool for symbolic controller
synthesis, to synthesize controllers for reachability and invariance speci cations on
four examples
