Případová studie paralelní verifikace komponentových systémů

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F08%3A00024171" target="_blank" >RIV/00216224:14330/08:00024171 - isvavai.cz</a>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

A Case Study in Parallel Verification of Component-Based Systems

Popis výsledku v původním jazyce

In large component-based systems, the applicability of formal verification techniques to check interaction correctness among components is becoming challenging due to the concurrency of a large number of components. In our approach, we employ parallel LTL-like model checking to handle the size of the model. We present the results of the actual application of the technique to the verification of a complex model of a real system created within the CoCoME Modelling Contest. In this case study, we check thevalidity of the model and the correctness of the system via checking various temporal properties. We concentrate on the component-specific properties, like local deadlocks of components, and correctness of given use-case scenarios.

Název v anglickém jazyce

A Case Study in Parallel Verification of Component-Based Systems

Popis výsledku anglicky

In large component-based systems, the applicability of formal verification techniques to check interaction correctness among components is becoming challenging due to the concurrency of a large number of components. In our approach, we employ parallel LTL-like model checking to handle the size of the model. We present the results of the actual application of the technique to the verification of a complex model of a real system created within the CoCoME Modelling Contest. In this case study, we check thevalidity of the model and the correctness of the system via checking various temporal properties. We concentrate on the component-specific properties, like local deadlocks of components, and correctness of given use-case scenarios.

Druh

J_x - Nezařazeno - Článek v odborném periodiku (Jimp, Jsc a Jost)

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í

2008

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 periodika

Electronic Notes in Theoretical Computer Science

ISSN

1571-0661

e-ISSN

—

Svazek periodika

220

Číslo periodika v rámci svazku

2

Stát vydavatele periodika

HU - Maďarsko

Počet stran výsledku

16

Strana od-do

—

Kód UT WoS článku

—

EID výsledku v databázi Scopus

—