S.D. Bruda and Z. Zhang (Canada)
tree logic, Failure trace testing
The two major systems of formal verification are model checking and model-based testing. Model checking is based on some form of temporal logic such as linear tempo ral logic (LTL) or computation tree logic (CTL). The most powerful and realistic logic being used is CTL, which is ca pable of expressing most interesting properties of processes such as liveness and safety. Model-based testing is based on some operational semantics of processes (such as traces and/or failures) and its associated preorders. The most fine grained preorder beside bisimulation (mostly of theoretical importance) is based on both failures and traces. We show that these two most powerful variants are equivalent, in the sense that for any failure trace test there exists a CTL for mula equivalent to it. Our result allows for parts of a large system to be specified logically while other parts are speci fied algebraically, thus combining the best of the two spec ification techniques.
Important Links:
Go Back
