Model Checking of Component Protocol Conformance – Optimizations by Reducing False Negatives

In past years, a number of works considered behavioral protocols of components and discussed approaches for automatically checking of compatibality of protocols (protocol conformance) in component-based systems. The approaches are usually model-checking approaches, i.e., a positive answer guarantees protocol conformance for all executions while a negative answer provides example executions that may lead to protocol violations. It turned out that if behavioral abstractions take into account unbounded concurrency and unbounded recursion, the protocol conformance checking problem becomes undecidable. There are two possibilities to overcome this problem: (i) further behavioral abstraction to finite state systems or (ii) a conservative approximation of the protocol conformance checking problem. Both approaches may lead to spurious counterexamples, i.e., due to abstractions or approximations the shown execution can never happen. This work considers the second approach and shows a heuristics that reduces the number of spurious counterexamples by cutting off search branches that definitely do not contain real counterexamples.