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

Direct link
A Global Algorithm for Model-Based Test Suite Generation
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems. (Testing of Reactive Systems)
2007 (English)In: Proc. 3rd Workshop on Model Based Testing: MBT 2007, Elsevier , 2007, 47-59 p.Conference paper (Refereed)
Place, publisher, year, edition, pages
Elsevier , 2007. 47-59 p.
, Electronic Notes in Theoretical Computer Science, ISSN 1571-0661 ; 190:2
National Category
Computer Science
URN: urn:nbn:se:uu:diva-95843DOI: 10.1016/j.entcs.2007.08.005OAI: oai:DiVA.org:uu-95843DiVA: diva2:170198
Available from: 2007-04-27 Created: 2007-04-27 Last updated: 2011-03-04Bibliographically 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

Other links

Publisher's full text

Search in DiVA

By author/editor
Hessel, AndersPettersson, Paul
By organisation
Computer Systems
Computer Science

Search outside of DiVA

GoogleGoogle Scholar

Altmetric score

Total: 235 hits
ReferencesLink to record
Permanent link

Direct link