Checking Primitive Component Behavior
| Thesis title in Czech: | Checking Primitive Component Behavior |
|---|---|
| Thesis title in English: | Checking Primitive Component Behavior |
| Academic year of topic announcement: | 2005/2006 |
| Thesis type: | diploma thesis |
| Thesis language: | angličtina |
| Department: | Department of Software Engineering (32-KSI) |
| Supervisor: | doc. RNDr. Jan Kofroň, Ph.D. |
| Author: | hidden - assigned and confirmed by the Study Dept. |
| Date of registration: | 11.11.2005 |
| Date of assignment: | 11.11.2005 |
| Date and time of defence: | 21.05.2007 00:00 |
| Date of electronic submission: | 21.05.2007 |
| Date of proceeded defence: | 21.05.2007 |
| Opponents: | doc. RNDr. Pavel Parízek, Ph.D. |
| Guidelines |
| 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? |
| References |
| [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 |