Enhanced Property Specification and Verification in BLAST

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F09%3A00207450" target="_blank" >RIV/00216208:11320/09:00207450 - isvavai.cz</a>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

Enhanced Property Specification and Verification in BLAST

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Enhanced Property Specification and Verification in BLAST

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

JC - Počítačový hardware a software

OECD FORD obor

—

Projekt

<a href="/cs/project/GA201%2F08%2F0266" target="_blank" >GA201/08/0266: Metody a modely pro ověřování konzistence aplikací založených na pokročilých komponentových modelech</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>Z - Vyzkumny zamer (s odkazem do CEZ)

Rok uplatnění

2009

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

FASE 2009 - Fundamental Approaches to Software Engineering

ISBN

978-3-642-00592-3

ISSN

—

e-ISSN

—

Počet stran výsledku

14

Strana od-do

—

Název nakladatele

Springer-Verlag

Místo vydání

—

Místo konání akce

Neuveden

Datum konání akce

1. 1. 2009

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

000265405500032