SGER: Convex Optimization of Lyapunov Certificates for Software Behavior Systems

SGER：软件行为系统的 Lyapunov 证书的凸优化

• 批准号: 0451865
• 负责人: Alexandre Megretski
• 金额: --
• 依托单位: Massachusetts Institute of Technology
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2004
• 资助国家: 美国
• 起止时间: 2004-09-15 至 2006-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0451865&HistoricalAwards=false
• 关键词: SGER; Convex; Optimization; Lyapunov; Certificates

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.

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