Partial Verification of Software Components: Heuristics for Environment Construction

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985807%3A_____%2F07%3A00090626" target="_blank" >RIV/67985807:_____/07:00090626 - isvavai.cz</a>

Alternative codes found

RIV/00216208:11320/07:10084053

Result on the web

—

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

Partial Verification of Software Components: Heuristics for Environment Construction

Original language description

Code model checking of software components suffers from the well-known problem of state explosion when applied to highly parallel components, despite the fact that a single component typically comprises a smaller state space than the whole system. We present a technique that addresses the problem of state explosion in code checking of primitive components with the Java PathFinder in case the checked property is absence of concurrency errors. The key idea is to reduce parallelism in the calling protocolon the basis of the information provided by static analysis searching for concurrency-related patterns in the component code; by a heuristic, some of the pattern instances are denoted as suspicious. Then, the environment (needed to be available since Java PathFinder checks only complete programs) is generated from a reduced calling protocol so that it exercises in parallel only those parts of the component?s code that likely contain concurrency errors.

Czech name

Částečná verifikace softwarových komponent: heuristiky pro konstrukci prostředí

Czech description

Při model checkingu kódu softwarových komponent, které se vyznačují vysokou úrovní paralelismu, se často vyskytne problem exploze stavového prostoru, bez ohledu na to, že jedna komponenta má obvykle menší stavový prostor než celý systém. Zde prezentujemetechniku, která adresuje problém exploze stavového prostoru pro ověřování kódu primitivních komponent s Java PathFinder v případě, že ověřovaná vlastnost je absence synchronizačních chyb. Klíčová myšlenka je redukce paralelismu ve volacím protokolu na základě informací poskytnutých statickou analýzou, která hledá v kódu komponenty vzory se vztahem k synchronizaci; pomocí heuristiky se některé patterny označí jako podezřelé. Potom se prostředí (potřebné, protože Java PathFinder ověřuje pouze kompletní Java programy) vygeneruje z redukovaného volacího protokolu tak, že se paralelně provádějí pouze ty části kódu komponenty, které pravděpodobně obsahují synchronizační chyby.

Type

D - Article in proceedings

CEP classification

JC - Computer hardware and software

OECD FORD branch

—

Project

Result was created during the realization of more than one project. More information in the Projects tab.

Continuities

Z - Vyzkumny zamer (s odkazem do CEZ)

Publication year

2007

Confidentiality

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

Article name in the collection

Proceedings of 33rd EUROMICRO SEAA Conference

ISBN

0-7695-2977-1

ISSN

—

e-ISSN

—

Number of pages

8

Pages from-to

75-82

Publisher name

IEEE Computer Society

Place of publication

Washington

Event location

Lübeck

Event date

Aug 28, 2007

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

—