Checking Compliance of Java Implementation with TBP Specification
| Thesis title in Czech: | Checking Compliance of Java Implementation with TBP Specification |
|---|---|
| Thesis title in English: | Checking Compliance of Java Implementation with TBP Specification |
| Academic year of topic announcement: | 2008/2009 |
| Thesis type: | diploma thesis |
| Thesis language: | angličtina |
| Department: | Department of Software Engineering (32-KSI) |
| Supervisor: | doc. RNDr. Pavel Parízek, Ph.D. |
| Author: | hidden - assigned and confirmed by the Study Dept. |
| Date of registration: | 06.05.2009 |
| Date of assignment: | 06.05.2009 |
| Date and time of defence: | 06.09.2010 00:00 |
| Date of electronic submission: | 06.09.2010 |
| Date of proceeded defence: | 06.09.2010 |
| Opponents: | doc. RNDr. Jan Kofroň, Ph.D. |
| Guidelines |
| The process of development of a software component consists of the following steps: (i) design of interfaces, (ii) definition of behavior specification (optional), (iii) implementation, and (iv) testing and verification (against the behavior specification, if available).
Threaded Behavior Protocols (TBP) is a formalism for behavior specification of software components that allows to specify valid sequences of method calls on component interfaces. It is the most recent member of a family of formalisms based on Behavior Protocols (BP). The main difference between TBP and original BP with respect to code checking is the support for state variables and explicit threads. We already have a tool for checking Java code against the original Behavior Protocols, which is based on combination of the Java PathFinder model checker and the Behavior Protocol Checker. The goal of this thesis is to create a tool for checking Java implementation of software components against behavior specification in TBP. The candidate will use (i) Java PathFinder for state space traversal of Java components and (ii) an existing library (TBPlib) for parsing TBP specifications and their transformation into finite automata. |
| References |
| 1. Java PathFinder, http://javapathfinder.sourceforge.net
2. J. Kofron, T. Poch, O. Sery. TBP: Code-Oriented Component Behavior Specification, Proceedings of SEW-32, IEEE CS, Oct 2008 3. P. Parizek, F. Plasil, J. Kofron. Model Checking of Software Components: Combining Java PathFinder and Behavior Protocol Model Checker, Proceedings of SEW-30, IEEE CS, 2007 |