Promotors: prof.dr. M.R. Mousavi (Halmstad University, SE) and prof.dr.ir. J.F. Groote (TU/e)
Co-promotor: dr.ir. T.A.C. Willemse (TU/e)
Eindhoven University of Technology
Date: 27 October, 16:00
Software quality has become an increasingly important concern in software development, as a consequence of the ever-ascending trend of using software systems in critical systems. Subsequently, testing as a technique for establishing a certain level of software quality has received much attention in the past decades. Model-based testing is a structured approach to testing. Using model-based testing the process of generating test-cases and predicting the correct outcome of test-cases (the so-called oracle problem) can be mechanized. By using rigorous models for system behavior, model-based testing is formalized in terms of a mathematical notion of conformance.
Input-output conformance (ioco) is a widely-studied and commonly-used conformance relation. The ioco relation is initially developed for the synchronous communication setting. It is also well-known that the ioco relation does not have the compositionality property. These characteristics can be an obstacle in testing of concurrent systems with the ioco relation. Concurrent systems are composed of interacting components which often communicate asynchronously with their environment. This thesis studies the characteristics of the ioco relation to make it suitable for testing of concurrent systems. In particular, we address the following topics.
- We look into the ioco relation from the computational point of view. It is shown that the problem of checking the ioco relation is PSPACE-COMPLETE. We present a polynomial time algorithm for deciding the ioco relation in a confined setting, namely for deterministic specifications.
- We investigate the testing power of the ioco relation in comparison with some other conformance relations in the literature. Originally, the ioco relation is developed for systems modeled as an input-output labeled transition system. We compare the ioco relation with the conformance relation introduced for internal-choice labeled transition system, and show that they are not equal.
- A comprehensive study of testing with the ioco relation in the asynchronous setting is conducted. In this regard, we characterize different subclasses of implementations and specifications with the same observational behavior, with respect to the ioco relation, in presence and absence of buffers. We show that the state-space explosion problem, caused by adding buffers to models in asynchronous setting, can be sidestepped by restricting either implementations or specifications to the presented subclasses.
- We study the property of decomposability of a specification with respect to the ioco relation. Decomposability allows for using the ioco relation in component-based and product-line software systems, where it is assumed that some parts of the system under development are reused components, which we collectively call platform. We define the property of decomposability on labeled transition systems formally, and consequently propose an algorithm to check that property. In this regard, we introduce the quotient automaton which is derived from a given specification with respect to the platform. We investigate the necessary and sufficient conditions for the validity of the quotient automaton, and prove that the conformance of any new component to the quotient automaton ensures the correctness of the whole system built up of the new component and the platform.