Coverage of Implementations by Simulating Specifications

Hana Chockler, Orna Kupferman

Research output: Chapter in Book/Report/Conference proceedingConference paperpeer-review

11 Citations (Scopus)

Abstract

In formal verification, we verify that an implementation is correct with respect to a specification. When verification succeeds and the implementation is proven to be correct, there is still a question of how complete the specification is, and whether it really covers all the behaviors of the implementation. In this paper we study coverage for simulation-based formal verification, where both the implementation and the specification are modelled by labeled state-transition graphs, and an implementation I satisfies a specification S if S simulates I. Our measure of coverage is based on small modifications we apply to I. A part of I is covered by S if the mutant implementation in which this part is modified is no longer simulated by S. Thus, “mutation coverage” tells us which parts of the implementation were actually essential for the success of the verification. We describe two algorithms for finding the parts of the implementation that are covered by S. The first algorithm improves a naive algorithm that checks the mutant implementations one by one by exploiting the significant overlaps among the mutant implementations. The second algorithm is symbolic, and it improves a naive symbolic algorithm by reducing the number of variables in the OBDDs involved. In addition, we compare our coverage measure with other approaches for measuring coverage.
Original languageEnglish
Title of host publicationFoundations of Information Technology in the Era of Networking and Mobile Computing, IFIP 17th World Computer Congress - TC1 Stream / 2nd IFIP International Conference on Theoretical Computer Science (TCS 2002)
PublisherKluwer Publishing
Pages409-421
Number of pages13
Volume223
Publication statusPublished - 2002

Fingerprint

Dive into the research topics of 'Coverage of Implementations by Simulating Specifications'. Together they form a unique fingerprint.

Cite this