Název: Software Component Verification: On Translating Behavior Protocols to Promela
Překlad názvu: Ověřování softwarových komponent: O překladu Behavior Protocols do Promely
Autoři: Kofroň, Jan
Typ dokumentu: Výzkumné zprávy
Rok: 2006
Jazyk: eng
Edice: Technical Report, svazek: 2006/11
Abstrakt: [eng] [cze]
Using 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. Používání softwarových komponent patří k moderním přístupům k vytváření rozšiřitelných a spolehlivých aplikací. K zajištění vysoké spolehlivost by komponentová aplikace měla být verifikována, např. podstoupit model checking. Implementace aplikace je většinou příliš složitá, než aby mohla být verifikována na formální úrovni. Proto se používá model, který je abstrakcí této implementace. Behavior Protocols jsou platformou pro modelování chování softwarových komponent. V tomto článku navrhujeme metodu pro překlad specifikace Behavior Protocols do Promely, která je následně použita jako vstup pro model checker Spin. Pokud máme model v jazyku Promela popisující chování komponent, můžeme efektivně ověřovat kompatibilitu i LTL vlastnosti kooperujících komponent.
Klíčová slova: behavior protocols; formal verification; PROMELA; software components
Číslo projektu: CEZ:AV0Z10300504 (CEP), GD201/05/H014 (CEP), 1ET400300504 (CEP)
Poskytovatel projektu: GA ČR, GA AV ČR

Instituce: Ústav informatiky AV ČR (web)
Informace o dostupnosti dokumentu: Dokument je dostupný v příslušném ústavu Akademie věd ČR.
Původní záznam: http://hdl.handle.net/11104/0148100

Trvalý odkaz NUŠL: http://www.nusl.cz/ntk/nusl-37380


Záznam je zařazen do těchto sbírek:
Věda a výzkum > AV ČR > Ústav informatiky
Zprávy > Výzkumné zprávy