Anzeige
Erschienen in:
2009 | OriginalPaper | Buchkapitel
Enhanced Property Specification and Verification in BLAST
verfasst von : Ondřej Šerý
Erschienen in: Fundamental Approaches to Software Engineering
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Model checking tools based on the iterative refinement of predicate abstraction (e.g.,
Slam
and
Blast
) often feature a specification language for expressing complex behavior rules. The source code under verification is instrumented by artificial variables and statements in order to transform the problem of checking such a rule into the problem of program location reachability. This way, the source code 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 state of the behavior rules aside from the source code instead of instrumenting them. We have implemented an extension to
Blast
, which accepts a specification language (a simplified version of
behavior protocols
), and checks its validity without modifying the input source code. An experiment with two Linux kernel drivers confirms the performance gain using the extension.