Témata prací (Výběr práce)Témata prací (Výběr práce)(verze: 336)
Detail práce
   Přihlásit přes CAS
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
Univerzita Karlova | Informační systém UK