Reactive Systems Group

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

PDF BIB

@InProceedings{Manna+others/98/Abstraction,
  author =    "Zohar Manna and Michael A. Col{\'o}n and Bernd Finkbeiner
               and Henny B. Sipma and Tom{\'a}s E. Uribe",
  title =     "Abstraction and Modular Verification of Infinite-State
               Reactive Systems",
  booktitle = "Requirements Targeting Software and Systems Engineering
	       (RTSE)",
  year =      1997,
  volume =    1526,
  editor =    "Manfred Broy and Bernhard Rumpe",
  series =    "LNCS",
  publisher = "Springer-Verlag",
  pages =     "273--292",
  location =  "Bernried, Germany"
}

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