Distributed Behavior Protocol Checker
| Název práce v češtině: | Distributed Behavior Protocol Checker |
|---|---|
| Název v anglickém jazyce: | Distributed Behavior Protocol Checker |
| 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í: | 10.11.2005 |
| Datum zadání: | 10.11.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: | RNDr. Jiří Adámek, Ph.D. |
| Zásady pro vypracování |
| The growth of the computability power in recent years has enabled practical use of model checking of software systems. However the state space explosion is still a serious problem that limits usage of this technique to relatively small tasks. One of the approaches that significantly decrease state space of the task is usage of behavior protocols [1] as a specification platform. A behavior protocol is a regular language that describes behavior of a software component so that component implementation details are hidden. However, even checking of behavior protocols compliance has to face the state space explosion problem. This is caused mainly by composing of the component often introduces parallelism to the resulting system.
Recent improvement of the behavior protocol checker [2] has increased the range of practically checkable application by decreasing both memory and time requirements. This tool is an on-the-fly model checker with a bit-based states' representation. Its usage is currently limited by time requirements only. One of the approaches, which should increase range of practical use of this technique even more, is distributed state space traversing. This approach corresponds well to the recent development of microprocessors as well. Goals: 1. Find suitable methods for dividing of the state space 2. Parallel traversing of the state space parts 3. Evaluating the size of the spate space traversed more than once Approach: 1. Find suitable properties of current state representation 2. Modify current state representation by adding new properties if needed 3. Use the properties to split state space into relatively independent areas processed by different computational nodes 4. Use the properties to prevent or detect traversal of already traversed areas |
| Seznam odborné literatury |
| [1] F. Plasil, S. Visnovsky: Behavior Protocols for Software Components. IEEE Transactions on Software Engineering, vol. 28, no. 11, Nov 2002
[2] Mach, M., Plasil, F., Kofron, J.: Behavior Protocol Verification: Fighting State Explosion, Published in the International Journal of Computer and Information Science, Vol.6, Number 1, ACIS, ISSN 1525-9293, pp. 22-30, Mar 2005 |