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

点击翻译按钮获取中文摘要

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