This exploratory research project is transferring innovative concepts and associated computational techniques from the control systems analysis arena to software engineering for embedded systems. The project seeks safer embedded systems by applying computational methods to obtain thoroughly tested software; better software certification methods (e.g. for aviation and medical applications); and new techniques for real-time applications. Specifically, the research brings concepts of Lyapunov invariance and associated computational procedures, widely applied in control theory, to the context of real-time, embedded software. The goal is to provide behavior certificates, in the form of numerical Lyapunov invariants, that the software will perform according to some desired specifications. The central idea of the research is to use techniques such as Lagrangian relaxation and convex optimization to produce certificates that (for example) all variables will remain within acceptable ranges and that, when so required, the program will finish in finite time. A considerable economic benefit is to be gained from partial automation of the software analysis process, in particular static analysis, and this research is expected to yield a broad new class of techniques for this purpose. Furthermore, the techniques being studied complement and extend emerging techniques for abstract interpretation of programs. The research pursues several specific objectives: development of dynamical system representations of software systems that are suitable for analysis via Lyapunov invariants, development of methods to compile relevant programs expressed in commonly used languages (such as C) into these dynamical system models; identification of Lyapunov-like invariants via linear programming and/or semidefinite programming to automatically establish key properties of software; definition and preliminary implementation of an automated software analysis tool, whose outputs are certificates of proper program behavior; adaptation of the above efforts to scale up to large computer programs; and finally implementation of the described methods on significant examples arising from the literature and from existing safety-critical software routinely used by MIT.
