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

9804100该研究解决了无限状态反应系统的属性验证问题，这些系统与其环境具有持续的相互作用。 反应式系统包括硬件、软件、实时和混合系统。 它们的计算可以被建模为无限状态序列，并且它们的属性可以方便地使用时序逻辑来表示。 除了非定时硬件，其中一个状态取决于一个固定的位数，这些系统是无限状态：不仅是一个计算状态的无限序列，但可能的系统状态的集合也是无限的。抽象是无限状态系统的所有演绎和算法验证技术的基础。算法方法探索状态空间的有限向量，这些向量通常是递增的。演绎验证规则也可以被理解为使用适当的抽象，使用中间断言来表达。当应用于软件系统时，在这两种情况下的主要挑战是找到正确的抽象，这将允许验证感兴趣的属性。 组合验证将复杂系统上的属性的有效性降低到较小组件上的相关属性的有效性。组合性通常与抽象一起使用，以验证比其他方式更大的系统。 该研究调查了新形式的抽象和组合推理，结合算法和演绎方法。 它们将促进软件组件的时间属性的验证，尽可能使过程自动化。

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.***