Modular Deductive-Algorithmic Verification of Hybrid Systems

混合系统的模块化演绎算法验证

基本信息

批准号：
9900984
负责人：
Zohar Manna
金额：
$ 27.5万
依托单位：
Stanford University
依托单位国家：
美国
项目类别：
Continuing Grant
财政年份：
1999
资助国家：
美国
起止时间：
1999-09-15 至 2002-11-30
项目状态：
已结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=9900984&HistoricalAwards=false
关键词：
Modular Deductive Algorithmic Verification Hybrid

项目摘要

9900984 Manna, Zohar Stanford UniversityTitle: Modular Deductive-Algorithmic Verification of Hybrid SystemsThe proposal describes techniques to integrate modular and deductive-algorithmic verification for reactive systems. The goal is to verify, more automatically, larger systems than is possible by either technique alone. The proposed techniques feature a tight integration of abstraction techniques and modular verification; they include: (1) Modular Deductive Model Checking: environmental assumptions needed to complete modular proofs are derived as part of the proof. (2) Modular Abstraction and Invariant Generation: invariants of modules are generated based on abstractions with different classes of assumptions on their environment. (3) Modular Techniques for Hybrid Systems: assumptions are generated for a continuously evolving environment. The proposed research will allow the partial verification of open systems, before their components are fully specified or their environment is known. Since these methods require less interaction, it is feasible to perform more checks on early versions of a system being designed. The techniques will be applicable to general infinite-state reactive systems. In particular, they will be applied to the challenging problems posed by hybrid systems. The techniques will be implemented in the framework of the STeP (Stanford Temporal Prover) verification system, and used to verify a complex hybrid system as a case study.

9900984 Manna，Zohar Stanford UniversityTitle：混合系统的模块化演绎算法验证该建议介绍了整合反应性系统的模块化和扣除式叠加验证的技术。目的是更自动验证比单独使用任何一种技术更大的系统。所提出的技术具有抽象技术和模块化验证的紧密整合。它们包括：（1）模块化演绎模型检查：完成模块化证明所需的环境假设是证明的一部分。（2）模块化抽象和不变生成：模块的不变性是基于对环境的假设不同类别的抽象生成的。（3）混合系统的模块化技术：为不断发展的环境生成假设。拟议的研究将允许对开放系统进行部分验证，然后才能完全指定其组件或已知其环境。由于这些方法需要较少的交互作用，因此可以对正在设计的系统的早期版本进行更多检查是可行的。该技术将适用于一般的无限国家反应性系统。特别是，它们将应用于混合系统带来的具有挑战性的问题。这些技术将在步骤（Stanford Perimal Prover）验证系统的框架内实施，并用来验证复杂的混合系统作为案例研究。