IBM Israel Research Seminars

In formal verification, we verify that a system is correct with respect to a specification. Even when the system 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 system. The challenge of making the verification process as exhaustive as possible is even more crucial in simulation-based verification, where the infeasible task of checking all input sequences is replaced by checking a test suite consisting of a finite subset of them. It is very important to measure the exhaustiveness of the test suite, and indeed, there has been an extensive research in the simulation-based verification community on coverage metrics, which provide such a measure. It turns out that no single measure can be absolute, leading to the development of numerous coverage metrics whose usage is determined by industrial verification methodologies.

I will introduce coverage metrics that seem more suitable for temporal logic model checking. Some of the metrics are an adaptation of the work done on coverage in simulation-based verification to the formal-verification setting. For each metric I will briefly describe an efficient algorithm for computing it.

I will also discuss possible applications of the study of causality and responsibility to coverage. I will show that coverage corresponds to counterfactual causality and that responsibility can be viewed as a refinement of coverage. It gives significant insight into unresolved issues regarding the definition of coverage and leads to potentially useful extensions of coverage.

Joint work with J.Y. Halpern, O. Kupferman, R. Kurshan, and M. Y. Vardi

About the Speaker
Hana Chockler is a Postdoctoral Research Associate at WPI (Worcester Polytechnic Institute) and a Visiting Scientist in the Theory of Distributed Systems group at MIT CSAIL. She completed her Ph.D. in Computer Science at Hebrew University under the guidance of Orna Kupferman. Her research interests are in formal verification, with emphasis on coverage metrics. Recently she became interested in verification of concurrent systems and in semantics of timing diagrams.