Abstract
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.
Original language | English |
---|---|
Awarding Institution |
|
Supervisors/Advisors |
|
Award date | 21 Mar 2007 |
Place of Publication | Enschede |
Publisher | |
Print ISBNs | 978-90-365-2476-6 |
Publication status | Published - 21 Mar 2007 |
Keywords
- EWI-9916
- METIS-241631
- FMT-TESTING
- IR-57810