  This article aims to provide a simple step-by-step guide highlighting the
steps needed to verify a control system with formal verification tools.
Starting from a description of the physical system and a control objective in
natural language, we design the plant and the controller, we use Simulink for
simulation and we employ a reachability analysis tool, SpaceEx, for formal
verification.
