SGER: Convex Optimization of Lyapunov Certificates for Software Behavior Systems

CNS 0451865 MIT Eric M.费隆标题：SGER：凸优化的Lyapunov证书的软件行为系统这个探索性的研究项目是转移创新的概念和相关的计算技术从控制系统分析竞技场的软件工程嵌入式系统。该项目通过应用计算方法获得经过彻底测试的软件，寻求更安全的嵌入式系统;更好的软件认证方法（例如航空和医疗应用）;以及实时应用的新技术。具体而言，研究带来的概念，李雅普诺夫不变性和相关的计算程序，广泛应用于控制理论，实时，嵌入式软件的背景下。目标是以数值李雅普诺夫不变量的形式提供行为证书，该软件将根据某些期望的规范执行。研究的中心思想是使用拉格朗日松弛和凸优化等技术来产生证书，（例如）所有变量将保持在可接受的范围内，并且当需要时，程序将在有限时间内完成。 从软件分析过程的部分自动化，特别是静态分析中获得了相当大的经济效益，预计这项研究将为此产生广泛的新技术。 此外，正在研究的技术补充和扩展新兴技术的抽象解释程序。 该研究追求几个具体目标：开发适合于通过李雅普诺夫不变量分析的软件系统的动力系统表示，开发用常用语言表达的相关程序的编译方法通过线性规划和/或半定规划识别类李雅普诺夫不变量，以自动建立软件的关键属性;自动化软件分析工具的定义和初步实现，其输出是正确的程序行为的证书;适应上述努力，以扩大到大型计算机程序;以及最后实现所描述的方法，从文献中产生的重要例子，并从现有的安全关键软件常规使用的麻省理工学院。

CNS 0451865 MIT Eric M. Feron Title: SGER: Convex Optimization of Lyapunov Certificates for Software Behavior SystemsThis 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.