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.

题目：混合系统的模块化演绎算法验证该提案描述了将反应系统的模块化和演绎算法验证集成在一起的技术。目标是比单独使用任何一种技术更自动地验证更大的系统。提出的技术特点是抽象技术和模块化验证的紧密集成；它们包括：(1)模演绎模型检验：推导完成模证明所需的环境假设，作为证明的一部分。(2)模块抽象和不变量生成：模块的不变量是基于对其环境具有不同类别假设的抽象而生成的。(3)混合系统的模块化技术：对不断变化的环境进行假设。拟议的研究将允许在其组件完全指定或其环境已知之前对开放系统进行部分验证。由于这些方法需要较少的交互，因此对正在设计的系统的早期版本执行更多的检查是可行的。这些技术将适用于一般的无限态反应系统。特别是，它们将被应用于混合系统带来的具有挑战性的问题。这些技术将在STeP （Stanford Temporal proof）验证系统的框架中实现，并用于验证一个复杂的混合系统作为案例研究。