|
| |
|
|
Jazyk pro rekonfiguraci runtime infrastruktury komponentových systémů
Malohlava, M. ; Bureš, Tomáš
A component system is not only composed of a model but also of an execution environment which is able to instantiate components described by the model. However, the execution environment reflecting a complex component model and its changes at runtime is a non-trivial and error-prone application. Hence it is beneficial to simplify and conceptualize the execution environment by having a simple way of describing component compositions and reconfigurations. In this paper we propose a minimalistic language which describes the composition of the component-based system’s infrastructure in a procedural way and thus reduces the execution environment basically to a simple language interpreter.
|
|
| |
|
| |
|
| |
|
|
Model checking softwarových komponent: úprava Java PathFinder pro spolupráci s Behavior Protocol Checker
Pařízek, P. ; Plášil, František ; Kofroň, Jan
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.
|
|
|
Rozšíření Behavior Protocols o data a multisynchronizaci
Kofroň, Jan
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.
|
|
|
Ověřování softwarových komponent: O překladu Behavior Protocols do Promely
Kofroň, Jan
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.
|
|
| |
|
|
Regresní měření výkonnosti projektu Mono
Kalibera, T. ; Bulej, Lubomír ; Tůma, P.
Regression benchmarking is a methodology for detecting performance changes in software by periodic benchmarking. This paper presents a statistical method for automated detection of performance changes and shows how this method performs on a prototype of a regression benchmarking suite for Mono.
|
guest ::
