Abstraction and Modular Verification of Infinite-State Reactive Systems
Zohar Manna, Michael A. Colón, Bernd Finkbeiner, Henny B. Sipma and Tomás E. Uribe
We review a number of temporal verification techniques for reactive systems using modularity and abstraction. Their use allows the verification of larger systems, and the incremental verification of systems as they are developed and refined. In particular, we show how deductive verification tools, and the combination of finite-state model checking and abstraction, allow the verification of infinite-state systems featuring data types commonly used in software specifications, including real-time and hybrid systems.
Requirements Targeting Software and Systems Engineering (RTSE) 1998 (RTSE 1998).