Automatic Control Software Synthesis for Quantized Discrete Time Hybrid Systems
Many Embedded Systems are indeed Software Based Control Systems (SBCSs). An SBCS consists of two main subsystems: the controller and the plant. Typically, the plant is a physical system consisting, for example, of mechanical or electrical devices whereas the controller consists of control software running on a microcontroller. In an endless loop, the controller reads sensor outputs from the plant and sends commands to plant actuators in order to guarantee that the closed loop system (that is, the system consisting of both plant and controller) meets given safety and liveness specifications (System Level Formal Specifications).