Space Effective Model Checking for Component-Interaction Automata

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F09%3A00028809" target="_blank" >RIV/00216224:14330/09:00028809 - isvavai.cz</a>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

Space Effective Model Checking for Component-Interaction Automata

Popis výsledku v původním jazyce

The techniques of component-based development are becoming a common practice in the area of software engineering. One of the crucial issues in the correctness of such systems is the correct interaction among the components. The formalism of component-interaction automata was devised to model various aspects of such interaction, as well as to allow automated verification in the form of model checking with properties expressed in the component-interaction LTL, a variant of the known linear temporal logic.As the state space of a component-based system can grow exponentially with the number of components, it is desirable to employ reduction techniques to make the verification task more feasible. In our work, we describe the implementation of the ample setpartial order reduction method within the component-interaction automata verification framework.

Název v anglickém jazyce

Space Effective Model Checking for Component-Interaction Automata

Popis výsledku anglicky

The techniques of component-based development are becoming a common practice in the area of software engineering. One of the crucial issues in the correctness of such systems is the correct interaction among the components. The formalism of component-interaction automata was devised to model various aspects of such interaction, as well as to allow automated verification in the form of model checking with properties expressed in the component-interaction LTL, a variant of the known linear temporal logic.As the state space of a component-based system can grow exponentially with the number of components, it is desirable to employ reduction techniques to make the verification task more feasible. In our work, we describe the implementation of the ample setpartial order reduction method within the component-interaction automata verification framework.

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

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

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

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

Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09)

ISBN

978-3-939897-15-6

ISSN

—

e-ISSN

—

Počet stran výsledku

8

Strana od-do

—

Název nakladatele

Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, Německo

Místo vydání

Dagstuhl, Německo

Místo konání akce

Znojmo, Česká republika

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

—