Engineering of Computer-Based Systems, IEEE International Conference on the (2003)
Apr. 7, 2003 to Apr. 10, 2003
Yifei Dong , State University of New York at Stony Brook
C. R. Ramakrishnan , State University of New York at Stony Brook
Scott A. Smolka , State University of New York at Stony Brook
We present an algebraic framework for evidence exploration: the process of interpreting, manipulating, and navigating the proof structure or evidence produced by a model checker when attempting to verify a system specification for a temporal-logic property. Due to the sheer size of such evidence, single-step traversal is prohibitive and smarter exploration methods are required. Evidence exploration allows users to explore evidence through smaller, manageable views, which are definable in relational graph algebra, a natural extension of relational algebra to graph structures such as model-checking evidence. We illustrate the utility of our approach by applying the Evidence Explorer, our tool implementation of the evidence-exploration framework, to the Java meta-locking algorithm, a highly optimized technique deployed by the Java Virtual Machine to ensure mutually exclusive access to object monitor queues by threads.
S. A. Smolka, Y. Dong and C. R. Ramakrishnan, "Model Checking and Evidence Exploration," Engineering of Computer-Based Systems, IEEE International Conference on the(ECBS), Huntsville, Alabama, 2003, pp. 214.