Original title: Software Component Verification: On Translating Behavior Protocols to Promela
Translated title: Ověřování softwarových komponent: O překladu Behavior Protocols do Promely
Authors: Kofroň, Jan
Document type: Research reports
Year: 2006
Language: eng
Series: Technical Report, volume: 2006/11
Abstract: [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.
Keywords: behavior protocols; formal verification; PROMELA; software components
Project no.: CEZ:AV0Z10300504 (CEP), GD201/05/H014 (CEP), 1ET400300504 (CEP)
Funding provider: GA ČR, GA AV ČR

Institution: Institute of Computer Science AS ČR (web)
Document availability information: Fulltext is available at the institute of the Academy of Sciences.
Original record: http://hdl.handle.net/11104/0148100

Permalink: http://www.nusl.cz/ntk/nusl-37380


The record appears in these collections:
Research > Institutes ASCR > Institute of Computer Science
Reports > Research reports