Checking Primitive Component Behavior
| Název práce v češtině: | Checking Primitive Component Behavior |
|---|---|
| Název v anglickém jazyce: | Checking Primitive Component Behavior |
| 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: | doc. RNDr. Jan Kofroň, Ph.D. |
| Řešitel: | skrytý - zadáno a potvrzeno stud. odd. |
| Datum přihlášení: | 11.11.2005 |
| Datum zadání: | 11.11.2005 |
| Datum a čas obhajoby: | 21.05.2007 00:00 |
| Datum odevzdání elektronické podoby: | 21.05.2007 |
| Datum proběhlé obhajoby: | 21.05.2007 |
| Oponenti: | doc. RNDr. Pavel Parízek, Ph.D. |
| Zásady pro vypracování |
| Software model checking is a process of checking for properties of a software application and thus assuring the software reliability. It becomes recently almost feasible as the computational power of today's systems has increased. Still it is necessary to divide the software application into pieces that are checked separately; the whole application yields an enormous state space that is impossible to traverse in a reasonable time. Therefore, the use of components for critical applications is a straightforward approach for dividing the entire application. Furthermore, as model checker usually works with a close code only, a suitable component environment need to be provided for each component.
Behavior protocols [1] are a method for component behavior specification. They allows for checking for components' behavior compatibility and compliance, used at the design time of an application to find possible architectural component misplacements. They are also suitable as a component behavior specification that can be compared with the behavior of the component implementation. The goal of the thesis is to provide a tool for comparing a primitive component behavior with its specification. Furthermore, a component environment generator using the component frame protocol will be implemented that would enable for checking for violation of the component behavior specification. The Java PathFinder model checker [2] and the Fractal component model [3] are to be used as a model checking platform. The solution of the proposed problem requires the following questions to be answered: * What's the most suitable way of detecting method calls and returns from the methods? * What part of the checked code should be modeled using MJI? * What's a suitable thread management approach? * How to deal with missing method parameters and return values within a behavior protocol? |
| Seznam odborné literatury |
| [1] F. Plášil, S. Višňovský: Behavior Protocols for Software Components. IEEE Transactions on Software Engineering, vol. 28, no. 11, Nov 2002
[2] Java PathFinder, http://javapathfinder.sourceforge.net/ [3] The Fractal Project, http://fractal.objectweb.org/ [4] Bernd Finkbeiner, Henny Sipma: Checking Finite Traces using Alternating Automata http://www-step.stanford.edu/papers/rv01.html |