Ověřování chování softwarových komponent pomocí Behavior Protocols a Spinu

Kód výsledku v IS VaVaI

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

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

Checking Software Component Behavior using Behavior Protocols and Spin

Popis výsledku v původním jazyce

sing software components is a modern approach for building extensible and reliable applications. To ensure high dependability, a component application should undergo verification, e.g. model checking, to prove it has certain properties. The implementation of an application is usually too complex to be verified at a formal level; therefore, a model being an abstraction of the implementation is to be used. Behavior protocols are a platform for modeling of software component behavior. In this paper, we propose a method for translation behavior protocols to Promela, which is consequently used as the input for the Spin model checker. Having the Promela code describing the component behavior, one can efficiently check for the behavior compatibility and LTL (Linear Temporal Logic) properties of cooperating software components.

Název v anglickém jazyce

Checking Software Component Behavior using Behavior Protocols and Spin

Popis výsledku anglicky

sing software components is a modern approach for building extensible and reliable applications. To ensure high dependability, a component application should undergo verification, e.g. model checking, to prove it has certain properties. The implementation of an application is usually too complex to be verified at a formal level; therefore, a model being an abstraction of the implementation is to be used. Behavior protocols are a platform for modeling of software component behavior. In this paper, we propose a method for translation behavior protocols to Promela, which is consequently used as the input for the Spin model checker. Having the Promela code describing the component behavior, one can efficiently check for the behavior compatibility and LTL (Linear Temporal Logic) properties of cooperating software components.

Druh

D - Stať ve sborníku

CEP obor

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

OECD FORD obor

—

Projekt

<a href="/cs/project/1ET400300504" target="_blank" >1ET400300504: Realistická aplikace formálních metod v komponentových systémech</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>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 the 2007 ACM Symposium on Applied Computing

ISBN

1-59593-480-4

ISSN

—

e-ISSN

—

Počet stran výsledku

5

Strana od-do

1513-1517

Název nakladatele

ACM

Místo vydání

New York

Místo konání akce

Seoul

Datum konání akce

11. 3. 2007

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

WRD - Celosvětová akce

Kód UT WoS článku

—