One of the primary purposes of embedded software and systems is to implement control algorithms aimed at harnessing the dynamics of complex dynamical systems, such as aircraft, automobiles, fast trains and automated transit systems. The necessity to certify these systems makes it a requirement to extract the semantics of the software as it interacts with the physical world. Several tools exist to achieve that goal, and they have displayed excellent performance when applied to large safety-critical software such as that present in avionics systems.
This presentation will be devoted to the contributions that control theory may bring to the extraction of useful control software semantics. It will be shown by means of examples that the process by which such semantics is obtained may be greatly simplified when working with control system specifications first. Numerical issues that arise when moving from the ideal world of system specifications to the concrete software environment will also be discussed.