Verification Runtime for SOFA

• Thesis title in English: Verification Runtime for SOFA
• Academic year of topic announcement: 2007/2008
• 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: 01.11.2007
• Date of assignment: 01.11.2007

Guidelines

SOFA is a modern component system, which provides the following features: hierarchical component model, component behavior specification and verification (via behavior protocols), distributed runtime environment, automatically generated connectors and support for SOA concepts.
The purpose of behavior verification in SOFA is, for a particular component application, (i) to detect communication errors between subcomponents of each composite component in the application, and (ii) to detect violations of certain properties by Java implementation of each primitive component; the supported properties of Java code are correspondence with the component behavior specification and absence of concurrency errors (e.g. deadlocks).
As for (ii), our current approach involves checking of each primitive component in isolation, since a single component typically generates a smaller state space than the whole application. Although in some cases it may be more efficient to check the whole component application as a single entity (i.e. as one Java program), the problem is that it is not possible to use standard runtime environment of SOFA in such a case, since it involves many advances features of Java (e.g. RMI and XML processing) that would make verification of Java code infeasible.

The goal of this thesis is to design and implement a lightweight runtime environment for SOFA ("verification runtime") that would allow feasible and efficient verification of complete component applications written in Java. In addition to that, the candidate should also implement a GUI front-end for the verification runtime and provide means for remote execution of verification tasks (e.g. on a cluster).
The Java PathFinder, which is a multi-purpose verification tool for Java byte code, is to be used as a model checking platform.

References

1. SOFA component model, http://sofa.objectweb.org
2. T. Bures, P. Hnetynka, F. Plasil, J. Klesnil, O. Kmoch, T. Kohan, P. Kotrc: Runtime Support for Advanced Component Concepts, Proceedings of SERA 2007, IEEE CS, pages 337-345
3. Java PathFinder, http://javapathfinder.sourceforge.net
4. Environment Generator for Java PathFinder, http://dsrg.mff.cuni.cz/projects/envgen