|
|
Application of Software Components in Operating System Design
Děcký, Martin ; Tůma, Petr (advisor) ; Döbel, Björn (referee) ; Sojka, Michal (referee)
This thesis describes the primary goal of the HelenOS microkernel multiserver operating system. The primary goal of the HelenOS project is to create a comprehensive research and development platform in the domain of general-purpose operating systems that would support state-of-the-art approaches and methods (such as verification of correctness) while at the same time focusing on practical relevance. The text of the thesis describes what specific means in terms of design (based on software components), implementation, development process and verification are used to achieve the primary goal. The thesis also evaluates the current state of HelenOS. Powered by TCPDF (www.tcpdf.org)
|
|
|
Heuristická redukce paralelismu v prostředí komponenty
Pařízek, P. ; Plášil, František
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.
|
|
|
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.
|
|
| |
|
| |
|
| |
|
| |
|
| |
guest ::
