« Cognitive Style of powerpoint | Main | Specification Coverage Aided Test Selection »
September 04, 2003
Guided search for CTL
System-dependent hints guide the expansion of states to reduce the size of intermediate BDDs in symbolic backward reachability analysis. Can obtain complete coverage with fewer computational resources. Property-dependent hints are what we have been using in our guided search. Property-dependent hints guide the serach into error states more quickly. Incidentally, structural-hints (defined in Grove, Visser paper below) guide the search into parts of the graph that are important to verify--regardless of the specific property.
[Symbolic guided search for CTL model checking, Roderick Bloem]
Hints are assertions on the input. Hints can restrict the behavior by pruning transitions out of a state. Hints can over-approximate behavior by allowing any transition that violates the hint to be taken. (page 2).
Hints can be property-dependent. Meaning they guide the search to errors. (p3)
Hints can be system-dependent. Meaning they address computation bottlenecks. (p3)
Only property dependent hints can be used in explicit MC. So system-dependent hints address bottlenecks while resulting in an exhaustive search that required less time/space. This isn't possible in explicit MC becaue the size of the state table is the same in the end either way.
The hints force backward computation to consider only states that results from certain instructions, rather than straying into parts of the state space with complicated dependencies. (sec 4, para 2).
Experimental results are good.
Posted by jones at September 4, 2003 11:38 AM
Comments
Post a comment
Thanks for signing in, . Now you can comment. (sign out)
(If you haven't left a comment here before, you may need to be approved by the site owner before your comment will appear. Until then, it won't appear on the entry. Thanks for waiting.)