Modular Deductive-Algorithmic Verification of Hybrid Systems

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

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.