Abstraction and Compositionality for the Verification of Infinite-State Reactive Systems

无限状态反应系统验证的抽象性和组合性

• 批准号: 9804100
• 负责人: Zohar Manna
• 金额: $ 8.5万
• 依托单位: Stanford University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 1998
• 资助国家: 美国
• 起止时间: 1998-10-01 至 1999-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9804100&HistoricalAwards=false
• 关键词: Abstraction; Compositionality; Verification; Infinite; State

9804100 The research addresses the verification of properties of infinite-state reactive systems, which have an ongoing interaction with their environment. Reactive systems include hardware, software, and real-time and hybrid systems. Their computations can be modeled as infinite sequences of states, and their properties conveniently expressed using temporal logic. Except for untimed hardware, where a state depends on a fixed number of bits, these systems are infinite-state: not only is a computation an infinite sequence of states, but the set of possible system states is infinite as well. Abstraction underlies virtually all deductive and algorithmic verification techniques for infinite-state systems.The algorithmic methods explore finite quotients of the state-space, which are often incrementally refined. Deductive verification rules can also be understood as using an appropriate abstraction, expressed using intermediate assertions. When applied to software systems, the main challenge in both cases is to find the right abstraction that will allow the verification of the properties of interest. Compositional verification reduces the validity of a property over a complex system to that of related properties over smaller components. Compositionality is often used together with abstraction to verify systems larger than would otherwise be possible. The research investigates new forms of abstraction and compositional reasoning, combining algorithmic and deductive methods. They will facilitate the verification of temporal properties of software components, automating the process whenever possible.***

9804100该研究涉及无限国家反应系统的性质的验证，这些系统与环境有着持续的相互作用。 反应性系统包括硬件，软件以及实时和混合系统。 它们的计算可以建模为状态的无限序列，并且它们的性质使用时间逻辑方便地表达。 除了不合时宜的硬件（状态取决于固定数量的位，这些系统都是无限状态：计算不仅是无限状态的序列，而且可能系统状态的集合也是无限的。抽象实际上是无限状态系统的所有演绎和算法验证技术。算法方法探索了状态空间的有限商，通常会逐步完善。演绎验证规则也可以理解为使用中间断言表示的适当抽象。当应用于软件系统时，两种情况下的主要挑战是找到可以验证感兴趣属性的正确抽象。 组成验证将属性对复杂系统的有效性降低到较小组件的相关特性的有效性。组成性通常与抽象一起使用，以验证系统比其他可能更大的系统。 该研究研究了新形式的抽象和组成推理，结合了算法和演绎方法。 它们将促进对软件组件的时间属性的验证，并尽可能自动化该过程。***