
Coverage Metrics for Model Checking
Hana Chockler(Author)
LAP Lambert Academic Publishing
Published on 26. July 2011
Book
Paperback/Softback
144 pages
978-3-8454-2198-8 (ISBN)
Description
This book considers formal verification of computerized systems. In formal verification (model checking),we verify the correctness of a system with respect to a desired behavior bychecking whether a mathematical model of the system satisfies a formal specification ofthe behavior. The process is fully automatic and, in case the verification fails, supplies a counterexample showing a behavior of the system that does not satisfy the specification. These counterexamples are very important and they can be essential in detecting subtle errors in complex designs. On the other hand, when the answer to the correctness query is positive, most model-checking tools terminate without further information to the user.Since a positive answer means that the system is correct with respect to the specification,this may seem like a reasonable policy. However, the exhaustiveness of the model checking process depends solely on the correctness and exhaustiveness of specifications, which are written manually. In this book, we study coverage metrics, which are a way to check exhaustiveness of specifications and can direct the verification process to unexplored areas of the design.
More details
Language
English
Place of publication
Germany
Product notice
Paperback (trade)
Unsewn / adhesive bound
Dimensions
Height: 220 mm
Width: 150 mm
Thickness: 9 mm
Weight
233 gr
ISBN-13
978-3-8454-2198-8 (9783845421988)
Copyright in bibliographic data and cover images is held by Nielsen Book Services Limited or by the publishers or by their respective licensors: all rights reserved.
Schweitzer Classification
Person
Hana Chockler received the the Ph.D. degree in computer science from the Hebrew University of Jerusalem, Israel in 2003. She joined the Formal Verification group at IBM Research Laboratory in Israel in 2005. Her research interests include automated formal verification of hardware and software systems and coverage metrics for formal verification.