Model checking tools based on the iterative predicate abstraction refinement (e.g., SLAM and BLAST) often feature a specification language for expressing complex behavior rules. The source codes under verification are instrumented by artificial variables and statements to transform the problem of checking such a rule into the problem of program location reachability. This way, the source codes get bloated and additional predicates have to be discovered and tracked during the verification. We suggest that a significant performance improvement can be achieved by tracking an explicit state of the behavior specification aside from the source codes instead of instrumenting them. For this purpose, we propose a specification language, a simplified version of behavior protocols, for expressing regular behavior rules and a prototype extension of BLAST, which tracks the explicit state of such a rule. Experiment with two Linux kernel drivers confirms the performance gain using the extension.
|Kolb, E., Sery, O., Weiss, R.: Applicability of the BLAST Model Checker: An Industrial Case Study,
Accepted for publication in the Proceedings of PSI'09, LNCS, Apr 2009
|Sery, O.: Enhanced Property Specification and Verification in BLAST,
In Proceedings of FASE 2009, LNCS 5503, pp. 456-469, York, UK, Mar 2009
All downloadable filed here are licensed under the BSD licence as well as the BLAST 2.4 release, which they are based on.
Modified BLAST source codes:
OPC UA Stack properties:
Back to home page