CSR - EHCS(EHS), TM: Abstract Interpretation-Based Analysis and Verification for Critical Systems

CSR - EHCS(EHS), TM：关键系统基于抽象解释的分析和验证

• 批准号: 0834535
• 负责人: Patrick Cousot
• 金额: --
• 依托单位: New York University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2008
• 资助国家: 美国
• 起止时间: 2008-09-01 至 2010-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0834535&HistoricalAwards=false
• 关键词: CSR; EHCS; EHS; TM; Abstract

Modern embedded critical systems are generally interactive and reactive, i.e. they are programs that interact with mechanical or electronic devices such as sensors and actuators. Errors in safety-critical and mission-critical programs (such as in the aviation arena) can be catastrophic. This research proposal identifies several areas in which the static analysis of critical systems using abstract interpretation can ensure the correctness of various aspects of critical systems. There are important issues in the analysis of critical systems for which abstract interpretation provides a promising approach. This research pursues analysis of liveness and responsiveness properties of critical systems. Most present-day static analyzers analyze safety properties, stating that no unwanted error can ever appear during any program execution. Recent work on termination has shown that abstract interpretation can also be useful in proving liveness properties like termination. Such liveness properties state that something good must eventually happen when the program is executed. In the context of reactive critical systems, an important liveness property is responsiveness: the program should react to an external event in a timely fashion. Abstract interpretation has proven to be a powerful method for verifying the safety properties of programs. On the other hand, temporal logic and its related methods provide ways for dealing with liveness properties of programs. An important aspect of the work proposed here is the integration of the two approaches in order to reason formally about a wide class of properties incorporating both safety and liveness. Furthermore, existing verification methods using abstraction are often restricted to finitary abstractions, i.e. abstractions into a finite domain. As another aspect of the proposed work, these verification methods will be extended to infinite domains. The research results are expected to have impact in a number of diverse areas. First, the new methodologies developed in the area of abstract interpretation as part of this research will provide the theoretical basis for future uses of static analysis to ensure the correctness of critical and embedded systems. Second, we anticipate the construction of software will be performed to extend the capability of current analyzers used in industry, such as the ASTRÉE system, to check increasingly important properties ? such as liveness and responsiveness of critical systems. Additionally, the proposed research will involve students at both the graduate and senior undergraduate level. Finally, the techniques developed will become part of the topics covered graduate courses in abstraction interpretation and verification.

现代嵌入式关键系统通常是交互式和反应性的，即它们是与传感器和执行器等机械或电子设备相互作用的程序。关键和关键任务计划（例如在航空领域）中的错误可能是灾难性的。该研究建议确定了几个领域，其中使用抽象解释对关键系统进行静态分析可以确保关键系统各个方面的正确性。在关键系统的分析中，抽象解释提供了一种有希望的方法。这项研究追求关键系统的耐受性和响应性能的分析。当今的大多数静态分析仪分析安全属性都表明，在任何程序执行过程中都不会出现不必要的错误。最近的终止工作表明，抽象的解释也可用于提供终止之类的能力。这种LIVISE属性指出，在执行程序时，必须最终发生一些好处。在反应性关键系统的背景下，重要的livestion属性是响应能力：该程序应及时对外部事件做出反应。事实证明，抽象解释是验证程序安全性能的有力方法。另一方面，临时逻辑及其相关方法提供了处理程序的LIVES属性的方法。这里提出的工作的一个重要方面是两种方法的整合，以正式理解包含安全性和livesice的广泛属性。此外，使用抽象的现有验证方法通常仅限于有限的抽象，即抽象成有限域。作为拟议工作的另一个方面，这些验证方法将扩展到无限领域。预计研究结果将在许多潜水员领域产生影响。首先，作为这项研究的一部分，在抽象解释领域开发的新方法将为静态分析的未来使用提供理论基础，以确保关键和嵌入式系统的正确性。其次，我们预计将执行软件的构建，以扩展行业中使用的当前分析仪（例如Astrée系统）检查日益重要的属性的能力？诸如关键系统的耐受性和响应能力。此外，拟议的研究将涉及研究生和高级本科生的学生。最后，开发的技术将成为涵盖抽象解释和验证的研究生课程的一部分。