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 ...
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 ...
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 ...
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
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
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
Specification and Generation of Environment for Model Checking of Software Compnents
Pařízek, P.; Plášil, František
2005 - English
Keywords:
software components; behavior protocols; model checking; automatic environment generation
Available at various institutes of the ASCR
Specification and Generation of Environment for Model Checking of Software Compnents
Enhancing Behavior Protocols with Atomic Actions
Kofroň, Jan
2005 - English
Keywords:
software components; behavior protocols; atomic actions; event synchronization
Available at various institutes of the ASCR
Enhancing Behavior Protocols with Atomic Actions
Handling Heterogeneity in Connector Generation
Galík, O.; Bureš, Tomáš
2005 - English
Keywords:
software connectors; code synthesis; heterogeneous deployment
Available at various institutes of the ASCR
Handling Heterogeneity in Connector Generation
Addressing Heterogeneity in OMG D&C-Based Deployment
Bulej, Lubomír; Bureš, Tomáš
2004 - English
Keywords:
OMG deployment; software connectors
Available at various institutes of the ASCR
Addressing Heterogeneity in OMG D&C-Based Deployment
NRGL provides central access to information on grey literature produced in the Czech Republic in the fields of science, research and education. You can find more information about grey literature and NRGL at service web
Send your suggestions and comments to nusl@techlib.cz
Provider
Other bases