Heuristic Reduction of Parallelism in Component Environment
Pařízek, P.; Plášil, František
2007 - English Code model checking of software components suffers from the well-known problem of state explosion when applied to highly parallel components, despite the fact that a single component typically comprises a smaller state space than the whole system. We present a technique that addresses the problem of state explosion in code checking of primitive components with the Java PathFinder in case the checked property is absence of concurrency errors. The key idea is reduction of parallelism in the environment so that only those parts of the component’s code that can likely cause concurrency errors are exercised in parallel; such parts are identified via a heuristic static code analysis (searching for “suspicious” patterns in the component code). Benefits of the technique, i.e. support for discovery of concurrency errors in limited time and space and provision of easy-to-read counterexamples, are illustrated on the results of several experiments. Při model checkingu kódu softwarových komponent, které se vyznačují vysokou úrovní paralelismu, se často vyskytne problem exploze stavového prostoru, bez ohledu na to, že jedna komponenta má obvykle menší stavový prostor než celý systém. Zde prezentujeme techniku, která adresuje problém exploze stavového prostoru pro ověřování kódu primitivních komponent s Java PathFinder v případě, že ověřovaná vlastnost je absence synchronizačních chyb. Klíčová myšlenka je redukce paralelismu v prostředí komponenty tak, že pouze ty části kódu komponenty, které pravděpodobně mohou vyvolat synchronizační chybu, jsou vykonány paralelně; takové části jsou identifikovány pomocí heuristické statické analýzy kódu (hledáním podezřelých vzorů v kódu komponenty). Výhody této techniky, t.j. podpora objevení synchronizačních chyb v omezeném čase a prostoru a reportování čitelnějších protipříkladů, jsou ilustrovány na výsledcích několika experimentů. Keywords: software components; model checking; concurrency errors; Java PathFinder; static analysis Available at various institutes of the ASCR Heuristic Reduction of Parallelism in Component Environment

Code model checking of software components suffers from the well-known problem of state explosion when applied to highly parallel components, despite the fact that a single component typically ...

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

Addressing Static Execution Overhead in Connectors with Disabled Optional Features
Bulej, Lubomír; Bureš, Tomáš
2006 - English Keywords: component systems; software connectors; runtime reconfiguration Available at various institutes of the ASCR Addressing Static Execution Overhead in Connectors with Disabled Optional Features

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

A Lower Bound Technique for Restricted Branching Programs (version F)
Žák, Stanislav
2006 - English Keywords: branching programs; lower bound Available at various institutes of the ASCR A Lower Bound Technique for Restricted Branching Programs (version F)

Žák, Stanislav
Ústav informatiky, 2006

Extending Behavior Protocols With Data and Multisynchronization
Kofroň, Jan
2006 - English 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. Keywords: behavior protocols; formal verification; software components Available at various institutes of the ASCR 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 - English 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: formal verification; software components; PROMELA; behavior protocols Available at various institutes of the ASCR 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 - English 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ý). Keywords: formal verification; software components; behavior protocols; Java PathFinder Available at various institutes of the ASCR 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 - English Keywords: software components; model checking; unbounded parallelism; behavior protocols Available at various institutes of the ASCR Modeling Unbounded Paralelism using Behavior Protocols

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

Rozbor faktorů ovlivňujících funkci přirozeného a umělého kloubu s ohledem na potřeby matematického modelování
Nedoma, Jiří
2005 - Czech Keywords: umělý kloub; matematické modelování Available at various institutes of the ASCR Rozbor faktorů ovlivňujících funkci přirozeného a umělého kloubu s ohledem na potřeby matematického modelování

Nedoma, Jiří
Ústav informatiky, 2005

Problems of influence of Car assistance systems on driving reliability and safety
Novák, Mirko
2005 - English Available at various institutes of the ASCR 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 - English Keywords: software components; software connectors; heterogeneous deployment Available at various institutes of the ASCR Deploying Heterogeneous Applications using OMG D&C and Software Connectors

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