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

Kód výsledku v 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>

Nalezeny alternativní kódy

RIV/00216208:11320/07:10084053

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

Partial Verification of Software Components: Heuristics for Environment Construction

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Partial Verification of Software Components: Heuristics for Environment Construction

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

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

OECD FORD obor

—

Projekt

Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.

Návaznosti

Z - Vyzkumny zamer (s odkazem do CEZ)

Rok uplatnění

2007

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

Proceedings of 33rd EUROMICRO SEAA Conference

ISBN

0-7695-2977-1

ISSN

—

e-ISSN

—

Počet stran výsledku

8

Strana od-do

75-82

Název nakladatele

IEEE Computer Society

Místo vydání

Washington

Místo konání akce

Lübeck

Datum konání akce

28. 8. 2007

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

WRD - Celosvětová akce

Kód UT WoS článku

—