Realizability of embedded controllers: from hybrid models to correct implementations

An embedded controller is a reactive device (e.g., a suitable combination of hardware and software components) that is embedded in a dynamical environment and has to react to environment changes in real time. Embedded controllers are widely adopted in many contexts of modern life, from automotive to avionics, from consumer electronics to medical equipment. Noticeably, the correctness of such controllers is crucial. When designing and verifying an embedded controller, often the need arises to model the controller and also its surrounding environment. The nature of the obtained system is hybrid because of the inclusion of both discrete-event (i.e., controller) and continuous-time (i.e., environment) processes whose dynamics cannot be characterized faithfully using either a discrete or continuous model only. Systems of this kind are named cyber-physical (CPS) or hybrid systems. Different types of models may be used to describe hybrid systems and they focus on different objectives: detailed models are excellent for simulation but not suitable for verification, high-level models are excellent for verification but not convenient for refinement, and so forth. Among all these models, hybrid automata (HA) [8, 77] have been proposed as a powerful formalism for the design, simulation and verification of hybrid systems. In particular, a hybrid automaton represents discrete-event processes by means of finite state machines (FSM), whereas continuous-time processes are represented by using real-numbered variables whose dynamics is specified by (ordinary) differential equation (ODE) or their generalizations (e.g., differential inclusions). Unfortunately, when the high-level model of the hybrid system is a hybrid automaton, several difficulties should be solved in order to automate the refinement phase in the design flow, because of the classical semantics of hybrid automata. In fact, hybrid automata can be considered perfect and instantaneous devices. They adopt a notion of time and evaluation of continuous variables based on dense sets of values (usually R, i.e., Reals). Thus, they can sample the state (i.e., value assignments on variables) of the hybrid system at any instant in such a dense set R≥0. Further, they are capable of instantaneously evaluating guard constraints or reacting to incoming events by performing changes in the operating mode of the hybrid system without any delay. While these aspects are convenient at the modeling level, any model of an embedded controller that relies for its correctness on such precision and instantaneity cannot be implemented by any hardware/software device, no matter how fast it is. In other words, the controller is un-realizable, i.e., un-implementable. This thesis proposes a complete methodology and a framework that allows to derive from hybrid automata proved correct in the hybrid domain, correct realizable models of embedded controllers and the related discrete implementations. In a realizable model, the controller samples the state of the environment at periodic discrete time instants which, typically, are fixed by the clock frequency of the processor implementing the controller. The state of the environment consists of the current values of the relevant variables as observed by the sensors. These values are digitized with finite precision and reported to the controller that may decide to switch the operating mode of the environment. In such a case, the controller generates suitable output signals that, once transmitted to the actuators, will effect the desired change in the operating mode. It is worth noting that the sensors will report the current values of the variables and the actuators will effect changes in the rates of evolution of the variables with bounded delays.