Theories for Model-based Testing: Real-time and Coverage

In the last years, increasingly complex systems are being put in charge of critical tasks. When these complex systems, are drive by sophisticated software, they need to attain a high degree of reliability. Unfortunately, developing correct systems is difficult, and in the past there have been several complex systems that went wrong because they lacked serious analysis of their potential behaviour. In this thesis, we study an effective way of obtaining confidence on the correctness of a system, known as testing. Testing is the systematic process of finding errors in a system by means of extensively experimenting with it. In order to successfully test a system, it is crucially needed to count with both effective test cases and feasible strategies to execute them. Fortunately, work in formal methods helps us achieving this task in a precise and rigorous manner. A particularly successful formal theory of testing is the ioco theory, devised by Tretmans to work on labelled input-output transition systems. The theory smoothly covers issues like nondeterminism and quiescence (that is, the notion representing the absence of outputs). The ioco testing theory is clean and precise, and is the basis used in successful testing tools, like the TORX tool and the TGV tool. In this thesis we extend the ioco testing theory in three important directions, as follows. Our first extension concerns the addition of real-time, which is crucial to the analysis of several systems (e.g., systems where actions are required to occur in a precise moment). New models and formalisms that take into account real-time are introduced. Furthermore,we develop a new testing relation between these real-time models, and a sound and exhaustive algorithm to derive tests for that relation. Our second extension arises when we consider the input and output actions as being subdivided in communication channels. We explore how these channels interact with realtime. Interestingly, this new setting is more flexible since it allows us to relax some standard assumptions. We develop a testing relation between models with real-time and channels, and a sound and exhaustive algorithm to derive tests for this new richer setting. Our third, final extension is concernedwith the common problemthat complete test suites usually cannot be covered in finite time for most interesting cases. Test coverage measures the proportion of the implementation exercised by a test suite. Existing coverage criteria are usually defined in terms of syntactic characteristics, having the disadvantage that behaviorally equivalent, although syntactically different systems have different measures. Moreover, these metrics do not take into account risks (i.e., values which represent that certain failures are more severe than others). We propose a novel approach for test coverage in a semantic style, where bisimilar processes measure equally. Moreover, we develop several algorithms to calculate tests with optimal coverage. The results presented in this thesis enrich the formal theory of testing. They provide a solid basis for make the process of testing more applicable, complete, and effective, helping today’s and tomorrow’s complex systems to be more reliable.