Extending BLAST with Behavior Protocols


Abstract

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.

Related Publications

PDF 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
PDF Sery, O.: Enhanced Property Specification and Verification in BLAST,
In Proceedings of FASE 2009, LNCS 5503, pp. 456-469, York, UK, Mar 2009

Download

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: blast-2.4_bp.tar.bz2(21MB)
Test files: tests.tar.bz2(315KB)
OPC UA Stack properties: psi09.tgz(1KB)


Back to home page