  We propose a hierarchical control framework for the synthesis of
correct-by-construction controllers for nonlinear control-affine systems with
respect to reach-avoid-stay specifications. We first create a low-dimensional
continuous abstraction of the system and use Sum-of-Squares (SOS) programming
to obtain a low-level controller ensuring a bounded error between the two
models. We then create a discrete abstraction of the continuous abstraction and
use formal methods to synthesize a controller satisfying the specifications
shrunk by the obtained error bound. Combining both controllers finally solves
the main control problem on the initial system. This two-step framework allows
the discrete abstraction methods to deal with higher-dimensional systems which
may be computationally expensive without the prior continuous abstraction. The
main novelty of the proposed SOS continuous abstraction is that it allows the
error between abstract and concrete models to explicitly depend on the control
input of the abstract model, which offers more freedom in the choice of the
continuous abstraction model and provides lower error bounds than when only the
states of both models are considered. This approach is illustrated on the
docking problem of a marine vessel.
