uu.seUppsala University Publications
Change search
ReferencesLink to record
Permanent link

Direct link
Model-Based Testing of a WAP Gateway: An Industrial Case-Study
Uppsala University, Teknisk-naturvetenskapliga vetenskapsområdet, Mathematics and Computer Science, Department of Information Technology.
2006 In: Technical Report 2006-045, (Extended version of a paper with the same name published in Brim L., Haverkort B., Leucker M., and van der Pol J., editors, Formal Methods: Applications and Technology, FMICS 2006 and PDMC 2006, LNCS 4346, pages 116--131, Springer 2007.), ISSN 1404-3203Article in journal (Refereed) Published
Place, publisher, year, edition, pages
URN: urn:nbn:se:uu:diva-95844OAI: oai:DiVA.org:uu-95844DiVA: diva2:170199
Available from: 2007-04-27 Created: 2007-04-27Bibliographically approved
In thesis
1. Model-Based Test Case Generation for Real-Time Systems
Open this publication in new window or tab >>Model-Based Test Case Generation for Real-Time Systems
2007 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

Testing is the dominant verification technique used in the software industry today. The use of automatic test case execution increases, but the creation of test cases remains manual and thus error prone and expensive. To automate generation and selection of test cases, model-based testing techniques have been suggested.

In this thesis two central problems in model-based testing are addressed: the problem of how to formally specify coverage criteria, and the problem of how to generate a test suite from a formal timed system model, such that the test suite satisfies a given coverage criterion. We use model checking techniques to explore the state-space of a model until a set of traces is found that together satisfy the coverage criterion. A key observation is that a coverage criterion can be viewed as consisting of a set of items, which we call coverage items. Each coverage item can be treated as a separate reachability problem.

Based on our view of coverage items we define a language, in the form of parameterized observer automata, to formally describe coverage criteria. We show that the language is expressive enough to describe a variety of common coverage criteria described in the literature. Two algorithms for test case generation with observer automata are presented. The first algorithm returns a trace that satisfies all coverage items with a minimum cost. We use this algorithm to generate a test suite with minimal execution time. The second algorithm explores only states that may increase the already found set of coverage items. This algorithm works well together with observer automata.

The developed techniques have been implemented in the tool CoVer. The tool has been used in a case study together with Ericsson where a WAP gateway has been tested. The case study shows that the techniques have industrial strength.

Place, publisher, year, edition, pages
Uppsala: Acta Universitatis Upsaliensis, 2007. 59 p.
Digital Comprehensive Summaries of Uppsala Dissertations from the Faculty of Science and Technology, ISSN 1651-6214 ; 301
Model-Based Testing, Model Checking, Coverage Criteria, Real-Time Systems, Black-Box Testing, Timed Automata, Test Case Generation, Conformance Testing
urn:nbn:se:uu:diva-7849 (URN)978-91-554-6883-5 (ISBN)
Public defence
2007-05-21, Polhemsalen, Ångström laboratory, Lägerhyddsvägen 1, Uppsala, 13:15
Available from: 2007-04-27 Created: 2007-04-27 Last updated: 2011-02-18Bibliographically approved

Open Access in DiVA

No full text

By organisation
Department of Information Technology

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Total: 298 hits
ReferencesLink to record
Permanent link

Direct link