Extending Java PathFinder with Behavior Protocols
| Název práce v češtině: | Extending Java PathFinder with Behavior Protocols |
|---|---|
| Název v anglickém jazyce: | Extending Java PathFinder with Behavior Protocols |
| Akademický rok vypsání: | 2005/2006 |
| Typ práce: | diplomová práce |
| Jazyk práce: | angličtina |
| Ústav: | Katedra softwarového inženýrství (32-KSI) |
| Vedoucí / školitel: | RNDr. Jiří Adámek, Ph.D. |
| Řešitel: | skrytý - zadáno a potvrzeno stud. odd. |
| Datum přihlášení: | 24.10.2005 |
| Datum zadání: | 24.10.2005 |
| Datum a čas obhajoby: | 11.09.2006 00:00 |
| Datum odevzdání elektronické podoby: | 11.09.2006 |
| Datum proběhlé obhajoby: | 11.09.2006 |
| Oponenti: | doc. RNDr. Jan Kofroň, Ph.D. |
| Zásady pro vypracování |
| Thesis categories: Problem analysis and solution proposal, implementation
Abstract Java PathFinder [1] is a model checker developed in NASA and intended for verification of behavior models written in Java. Its purpose is to decide whether given properties are satisfied for a given Java program. A property can be described either by an assertion inserted into the Java program, or by a Java class, that acts as a listener subscribed to the events produced by the state-space searching algorithm (a part of Java PathFinder). Using those listeners, Java PathFinder can be extended to check for complex behavior properties. Behavior protocols [2,3] were developed as a behavior specification language for hierarchical software components. Prototype implementation of the behavior protocol checker was developed for the SOFA [4] and Fractal [5] component models. In a hierarchical component system, each component is either composite (i.e. it is created as a composition of lower-level components) or primitive (implemented directly in a common programming language, e.g. Java). With each component, a behavior protocol is associated. To support design of composite components, behavior protocols allow to check for the behavior compliance [2] between adjacent levels of component hierarchy and for the (absence of) composition errors [3]. In order to (statically) verify behavior of the whole component application, it is necessary to also check compliance between the code of a primitive component and its behavior protocol. Therefore, the aim of this master thesis is to extend Java PathFinder in order to check compliance of a Fractal [5] primitive component code with a behavior protocol. Here, the behavior protocol serves both as the component behavior specification and the component environment behavior specification. Expected outputs Prototype implementation based on Java PathFinder |
| Seznam odborné literatury |
| [1] Java PathFinder, http://javapathfinder.sourceforge.net/
[2] F. Plasil, S. Visnovsky: Behavior Protocols for Software Components. IEEE Transactions on Software Engineering, vol. 28, no. 11, Nov 2002 [3] J. Adamek, F. Plasil: Component Composition Errors and Update Atomicity: Static Analysis. Accepted for publication in the Journal of Software Maintenance and Evolution: Research and Practice, 2004 [4] The SOFA project, http://sofa.objectweb.org/ [5] The Fractal Project, http://fractal.objectweb.org/ |
| Předběžná náplň práce |
| The aim of the thesis is to extend the Java PathFinder model checker in order to check compliance of a Fractal primitive component code with a behavior protocol. |