Extending Behavior Protocols With Data and Multisynchronization
Kofroň, Jan
2006 - anglický Using behavior protocol for behavior specification of components in hierarchical components model (SOFA, Fractal) turned out to be very beneficial if one is interested in communication errors among the application components. Recently, during specification of a Fractal component application aimed at controlling the access to the Internet at airports allowing for several types of payments for the access, several issues regarding the behavior protocols as a specification platform have arisen. The two most important are (i) insufficient expensiveness of behavior protocol language when specifying some typical behavior patterns, and (ii) insufficient performance of the behavior protocol checker – a tool used for searching for composition errors among communicating components. This paper focuses on solution of the first issue by proposing several extensions to behavior protocols. Použití Behavior Protocols pro specifikaci chování komponent v hierarchických komponentových modelech (SOFA, Fractal) se ukázalo být vhodným přístupem, pokud nás zajímá absence komunikačních chyb mezi komponentami v dané aplikaci. Během specifikace Fractalové komponentové aplikace zaměřené na kontrolu přístupu k internetu na letištích umožňující několik způsobů úhrady se projevilo několik nedostatků Behavior Protocols jako specifikační platformy. Dvě nejdůležitější zahrnují (i) nedostatečná vyjadřovací síla Behavior Protocols při specifikaci některých běžných vzorů chování a (ii) nedostatečný výkon aplikace Behavior Protocol Checker – nástroje použitého pro hledání kompozičních chyb mezi komunikujícími komponentami. Tento článek se soustředí na řešení prvního problému pomocí rozšíření formalismu Behavior Protocols. Klíčová slova: behavior protocols; formal verification; software components Plné texty jsou dostupné na jednotlivých ústavech Akademie věd ČR. Extending Behavior Protocols With Data and Multisynchronization

Using behavior protocol for behavior specification of components in hierarchical components model (SOFA, Fractal) turned out to be very beneficial if one is interested in communication errors among ...

Kofroň, Jan
Ústav informatiky, 2006

Software Component Verification: On Translating Behavior Protocols to Promela
Kofroň, Jan
2006 - anglický 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: formal verification; software components; PROMELA; behavior protocols Plné texty jsou dostupné na jednotlivých ústavech Akademie věd ČR. Software Component Verification: On Translating Behavior Protocols to Promela

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 ...

Kofroň, Jan
Ústav informatiky, 2006

Model Checking of Software Components: Making Java PathFinder Cooperate with Behavior Protocol Checker
Pařízek, P.; Plášil, František; Kofroň, Jan
2006 - anglický Although there exist several software model checkers that check the code against properties specified e.g. via a temporal logic and assertions, or just verifying low-level properties (like unhandled exceptions), none of them supports checking of software components against a high-level behavior specification. We present our approach to model checking of software components implemented in Java against a high-level specification of their behavior defined via behavior protocols 1 which employs the Java PathFinder model checker and the protocol checker. The property checked by the Java PathFinder (JPF) tool (correctness of particular method call sequences) is validated via its cooperation with the protocol checker. We show that just the publisher/listener pattern claimed to be the key flexibility support of JPF (even though proved very useful for our purpose) was not enough to achieve this kind of checking. Přestože existuje několik model checkerů pro software, které ověřují kód proti specifikaci zapsané např. v temporální logice a tzv. assertions, nebo ověřují nízkoúrovňové vlastnosti (jako neošetřené výjimky), žádný z nich nepodporuje ověřování softwarových komponent proti vyšší specifikaci chování. Tato zpráva popisuje náš přístup k model checkingu softwarových komponent implementovaných v jazyce Java proti specifikaci jejich chování definované pomocí protokolů chování, který využívá model checker Java PathFinder a protocol checker. Vlastnosti ověřované nástrojem Java PathFinder (korektnost sekvencí volání metod) se validují pomocí spolupráci s nástrojem protocol checker. Ukazujeme, že pouze návrhový vzor publisher/listener, označovaný za klíčový pro podporu rozšiřitelnosti v nástroji Java PathFinder, nebyl dostatečný pro tento typ ověřování (přestože byl pro nás velmi užitečný). Klíčová slova: formal verification; software components; behavior protocols; Java PathFinder Plné texty jsou dostupné na jednotlivých ústavech Akademie věd ČR. Model Checking of Software Components: Making Java PathFinder Cooperate with Behavior Protocol Checker

Although there exist several software model checkers that check the code against properties specified e.g. via a temporal logic and assertions, or just verifying low-level properties (like unhandled ...

Pařízek, P.; Plášil, František; Kofroň, Jan
Ústav informatiky, 2006

Modeling Unbounded Paralelism using Behavior Protocols
Adámek, Jiří
2005 - anglický Klíčová slova: software components; model checking; unbounded parallelism; behavior protocols Plné texty jsou dostupné na jednotlivých ústavech Akademie věd ČR. Modeling Unbounded Paralelism using Behavior Protocols

Adámek, Jiří
Ústav informatiky, 2005

Problems of influence of Car assistance systems on driving reliability and safety
Novák, Mirko
2005 - anglický Plné texty jsou dostupné na jednotlivých ústavech Akademie věd ČR. Problems of influence of Car assistance systems on driving reliability and safety

Novák, Mirko
Ústav informatiky, 2005

Deploying Heterogeneous Applications using OMG D&C and Software Connectors
Bulej, Lubomír; Bureš, Tomáš
2005 - anglický Klíčová slova: software components; software connectors; heterogeneous deployment Plné texty jsou dostupné na jednotlivých ústavech Akademie věd ČR. Deploying Heterogeneous Applications using OMG D&C and Software Connectors

Bulej, Lubomír; Bureš, Tomáš
Ústav informatiky, 2005

Specification and Generation of Environment for Model Checking of Software Compnents
Pařízek, P.; Plášil, František
2005 - anglický Klíčová slova: software components; behavior protocols; model checking; automatic environment generation Plné texty jsou dostupné na jednotlivých ústavech Akademie věd ČR. Specification and Generation of Environment for Model Checking of Software Compnents

Pařízek, P.; Plášil, František
Ústav informatiky, 2005

Enhancing Behavior Protocols with Atomic Actions
Kofroň, Jan
2005 - anglický Klíčová slova: software components; behavior protocols; atomic actions; event synchronization Plné texty jsou dostupné na jednotlivých ústavech Akademie věd ČR. Enhancing Behavior Protocols with Atomic Actions

Kofroň, Jan
Ústav informatiky, 2005

Handling Heterogeneity in Connector Generation
Galík, O.; Bureš, Tomáš
2005 - anglický Klíčová slova: software connectors; code synthesis; heterogeneous deployment Plné texty jsou dostupné na jednotlivých ústavech Akademie věd ČR. Handling Heterogeneity in Connector Generation

Galík, O.; Bureš, Tomáš
Ústav informatiky, 2005

Addressing Heterogeneity in OMG D&C-Based Deployment
Bulej, Lubomír; Bureš, Tomáš
2004 - anglický Klíčová slova: OMG deployment; software connectors Plné texty jsou dostupné na jednotlivých ústavech Akademie věd ČR. Addressing Heterogeneity in OMG D&C-Based Deployment

Bulej, Lubomír; Bureš, Tomáš
Ústav informatiky, 2004