Modular Deductive-Algorithmic Verification of Hybrid Systems

9900984 吗哪 斯坦福大学混合系统的模块化演绎算法验证该提案描述了集成模块化和演绎算法验证反应式系统的技术。 其目标是更自动地验证更大的系统，而不是单独使用任何一种技术。 所提出的技术的特点是一个紧密结合的抽象技术和模块化验证，他们包括：（1）模块演绎模型检查：完成模块化证明所需的环境假设推导的证明的一部分。 (2)模块化抽象和不变量生成：模块的不变量是基于对其环境的不同类别的假设的抽象而生成的。(3)混合系统的模块化技术：假设是为一个不断发展的环境而产生的。 拟议的研究将允许部分验证开放系统，在其组件被完全指定或其环境是已知的。由于这些方法需要较少的交互，因此可以对正在设计的系统的早期版本进行更多的检查。 该技术将适用于一般的无限状态反应系统。 特别是，他们将被应用到混合动力系统所带来的挑战性问题。这些技术将在STeP（斯坦福大学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.