Modeling Environment for Component Model Checking from Hierarchical Architecture

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F07%3A00005152" target="_blank" >RIV/00216208:11320/07:00005152 - isvavai.cz</a>

Alternative codes found

RIV/67985807:_____/07:00090203

Result on the web

—

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

Modeling Environment for Component Model Checking from Hierarchical Architecture

Original language description

Application of model checking to isolated software components is not directly possible because a component does not form a complete program - the problem of missing environment occurs. A solution is to create an environment of some form for the componentsubject to model checking. As the most general environment can cause model checking of the component to be infeasible, we model the environment on the basis of a particular context the component is to be used in. More specifically, our approach exploitshierarchical component architecture and component behavior specification defined via behavior protocols, all that provided in ADL. This way, the environment represents the behavior of the rest of the particular application with respect to the target component. We present an algorithm for computing the model of environment?s behavior that is based on syntactical expansion and substitution of behavior protocols.

Czech name

Modelování prostředí pro model checking komponent z hierarchických architektur

Czech description

Aplikace model checkingu na izolované softwarové komponenty není přímo možná, protože komponenta netvoří kompletní program - nastává problém chybějícího prostředí. Řešením je vytvoření nějakého prostředí pro komponentu, kterou chceme ověřovat. Protože nejobecnější možné prostředí může způsobit nezvladatelnost ověřování komponenty, modelujeme prostředí na základě specifického kontextu, ve kterém se komponenta použije. Konkrétně, naše řešení využívá hierarchickou komponentovou architekturu a specifikaci chování komponenty definovanou pomocí protokolů chování, všechno poskytované v ADL. Prostředí pak reprezentuje chování zbytku aplikace vzhledem k cílové komponentě. Zpráva dále popisuje algoritmus pro výpočet modelu chování pro prostředí, který je založenna syntaktické expanzi a substituci protokolu chování.

Type

J_x - Unclassified - Peer-reviewed scientific article (Jimp, Jsc and Jost)

CEP classification

JC - Computer hardware and software

OECD FORD branch

—

Project

<a href="/en/project/GA201%2F06%2F0770" target="_blank" >GA201/06/0770: Formal methods applicable to development of component-based systems</a><br>

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ů

Name of the periodical

Electronic Notes in Theoretical Computer Science

ISSN

1571-0661

e-ISSN

—

Volume of the periodical

182

Issue of the periodical within the volume

Neuveden

Country of publishing house

US - UNITED STATES

Number of pages

15

Pages from-to

139-153

UT code for WoS article

—

EID of the result in the Scopus database

—