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

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

基本信息

  • 批准号:
    0834535
  • 负责人:
  • 金额:
    --
  • 依托单位:
  • 依托单位国家:
    美国
  • 项目类别:
    Standard Grant
  • 财政年份:
    2008
  • 资助国家:
    美国
  • 起止时间:
    2008-09-01 至 2010-08-31
  • 项目状态:
    已结题

项目摘要

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.
现代嵌入式关键系统通常是交互式和反应式的,即它们是与机械或电子设备(如传感器和执行器)交互的程序。安全关键和任务关键程序(如航空竞技场)中的错误可能是灾难性的。 这个研究建议确定了几个领域,在这些领域中,使用抽象解释的关键系统的静态分析可以确保关键系统的各个方面的正确性。 有重要的问题,在分析的关键系统,抽象的解释提供了一个有前途的方法。 本研究致力于分析关键系统的活性和响应特性。 目前大多数静态分析器分析安全属性,说明在任何程序执行期间都不会出现不必要的错误。最近关于终止性的研究表明,抽象解释在证明活性性质(如终止性)方面也很有用。这种活性属性表明,当程序执行时,最终一定会发生一些好的事情。在反应式关键系统的背景下,一个重要的活性属性是响应性:程序应该及时对外部事件做出反应。 抽象解释已被证明是验证程序安全性的一种有效方法。另一方面,时态逻辑及其相关方法提供了处理程序活性特性的方法。这里提出的工作的一个重要方面是整合这两种方法,以正式的理由广泛的一类属性,包括安全性和活性。此外,使用抽象的现有验证方法通常限于有限抽象,即抽象到有限域中。作为所提出的工作的另一个方面,这些验证方法将被扩展到无限域。 研究结果预计将在许多不同领域产生影响。首先,作为本研究的一部分,在抽象解释领域开发的新方法将为未来使用静态分析提供理论基础,以确保关键和嵌入式系统的正确性。 第二,我们预计软件的建设将被执行,以扩大目前的分析仪在工业中使用的能力,如ASTRÉE系统,检查越来越重要的属性?例如关键系统的活性和响应性。此外,拟议的研究将涉及研究生和高年级本科生。最后,开发的技术将成为抽象解释和验证研究生课程所涵盖的主题的一部分。

项目成果

期刊论文数量(0)
专著数量(0)
科研奖励数量(0)
会议论文数量(0)
专利数量(0)

数据更新时间:{{ journalArticles.updateTime }}

{{ item.title }}
{{ item.translation_title }}
  • DOI:
    {{ item.doi }}
  • 发表时间:
    {{ item.publish_year }}
  • 期刊:
  • 影响因子:
    {{ item.factor }}
  • 作者:
    {{ item.authors }}
  • 通讯作者:
    {{ item.author }}

数据更新时间:{{ journalArticles.updateTime }}

{{ item.title }}
  • 作者:
    {{ item.author }}

数据更新时间:{{ monograph.updateTime }}

{{ item.title }}
  • 作者:
    {{ item.author }}

数据更新时间:{{ sciAawards.updateTime }}

{{ item.title }}
  • 作者:
    {{ item.author }}

数据更新时间:{{ conferencePapers.updateTime }}

{{ item.title }}
  • 作者:
    {{ item.author }}

数据更新时间:{{ patent.updateTime }}

Patrick Cousot其他文献

Abstract Interpretation: From 0, 1, To ∞
抽象解读:从0、1、到无穷大
  • DOI:
  • 发表时间:
    2022
  • 期刊:
  • 影响因子:
    0
  • 作者:
    Patrick Cousot
  • 通讯作者:
    Patrick Cousot
Sometime = always + recursion ≡ always on the equivalence of the intermittent and invariant assertions methods for proving inevitability properties of programs
  • DOI:
    10.1007/bf00290704
  • 发表时间:
    1987-02-01
  • 期刊:
  • 影响因子:
    0.500
  • 作者:
    Patrick Cousot;Radhia Cousot
  • 通讯作者:
    Radhia Cousot

Patrick Cousot的其他文献

{{ item.title }}
{{ item.translation_title }}
  • DOI:
    {{ item.doi }}
  • 发表时间:
    {{ item.publish_year }}
  • 期刊:
  • 影响因子:
    {{ item.factor }}
  • 作者:
    {{ item.authors }}
  • 通讯作者:
    {{ item.author }}

{{ truncateString('Patrick Cousot', 18)}}的其他基金

SHF: Small: Semantics, Static Analysis, and Refencing of Concurrent Programs with Weak Memory Models
SHF:小型:具有弱内存模型的并发程序的语义、静态分析和引用
  • 批准号:
    1617717
  • 财政年份:
    2016
  • 资助金额:
    --
  • 项目类别:
    Standard Grant
CPS: Breakthrough: Cyber-Physical System Securitization by Responsibility Analysis
CPS:突破:通过责任分析实现信息物理系统安全化
  • 批准号:
    1446511
  • 财政年份:
    2015
  • 资助金额:
    --
  • 项目类别:
    Standard Grant

相似海外基金

CSR-EHCS(EHS), SM: Collaborative Research: An Anytime Approach to Real-Time Embedded Control
CSR-EHCS(EHS),SM:协作研究:实时嵌入式控制的随时方法
  • 批准号:
    0834771
  • 财政年份:
    2008
  • 资助金额:
    --
  • 项目类别:
    Standard Grant
Collaborative Research: CSR-EHCS(EHS), TM: Distributed Sensing via Robust Consensus on Manifolds
合作研究:CSR-EHCS(EHS),TM:通过流形上的鲁棒共识进行分布式传感
  • 批准号:
    0834470
  • 财政年份:
    2008
  • 资助金额:
    --
  • 项目类别:
    Standard Grant
CSR-EHCS (EHS), TM: Compositional Technology for Safety-Critical Modular Systems
CSR-EHCS (EHS),TM:安全关键型模块化系统的组合技术
  • 批准号:
    0834409
  • 财政年份:
    2008
  • 资助金额:
    --
  • 项目类别:
    Standard Grant
CSR-EHCS(EHS), SM: Collaborative Research: An Anytime Approach to Real-Time Embedded Control
CSR-EHCS(EHS),SM:协作研究:实时嵌入式控制的随时方法
  • 批准号:
    0834661
  • 财政年份:
    2008
  • 资助金额:
    --
  • 项目类别:
    Standard Grant
CSR-EHCS(EHS), SM: Efficient Dynamic Combinatorial Models (EDCM) for Reliability Analysis of Complex Dynamic Systems
CSR-EHCS(EHS)、SM:用于复杂动态系统可靠性分析的高效动态组合模型 (EDCM)
  • 批准号:
    0832594
  • 财政年份:
    2008
  • 资助金额:
    --
  • 项目类别:
    Standard Grant
Collaborative Research: CSR-EHCS(EHS), TM: Distributed Sensing via Robust Consensus on Manifolds
合作研究:CSR-EHCS(EHS),TM:通过流形上的鲁棒共识进行分布式传感
  • 批准号:
    0834446
  • 财政年份:
    2008
  • 资助金额:
    --
  • 项目类别:
    Standard Grant
CSR-EHCS(EHS), SM: Investigating a Novel Embedded Processor Architecture for Electonic Textiles in Wearable and Pervasive Computing
CSR-EHCS(EHS)、SM:研究可穿戴和普适计算中电子纺织品的新型嵌入式处理器架构
  • 批准号:
    0834490
  • 财政年份:
    2008
  • 资助金额:
    --
  • 项目类别:
    Standard Grant
CSR-EHCS(EHS), SM: Development of SYMBIOTE, A Reconfigurable Logic Assisted Data Stream Management System for Multimedia Sensor Networks
CSR-EHCS(EHS)、SM:SYMBIOTE 的开发,一种用于多媒体传感器网络的可重构逻辑辅助数据流管理系统
  • 批准号:
    0834682
  • 财政年份:
    2008
  • 资助金额:
    --
  • 项目类别:
    Standard Grant
CSR-EHCS(EHS), SM: Collaborative Research: Integrated Energy-Aware Resource Scheduling for Wireless Real-Time Systems
CSR-EHCS(EHS)、SM:协作研究:无线实时系统的集成能源感知资源调度
  • 批准号:
    0834230
  • 财政年份:
    2008
  • 资助金额:
    --
  • 项目类别:
    Standard Grant
CSR-EHCS(EHS), SM: Collaborative Research: Integrated Energy-Aware Resource Scheduling for Wireless Real-Time Systems
CSR-EHCS(EHS)、SM:协作研究:无线实时系统的集成能源感知资源调度
  • 批准号:
    0834180
  • 财政年份:
    2008
  • 资助金额:
    --
  • 项目类别:
    Standard Grant
{{ showInfoDetail.title }}

作者:{{ showInfoDetail.author }}

知道了