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