Model-based testing with labeled transition systems

August 14, 2006
Jan Tretmans | Embedded Systems Institute, the Netherlands

Systematic testing of software plays an important role in the quest for improved software quality. Testing, however, turns out to be an error-prone, expensive, and time-consuming process. Model based testing is one of the promising technologies to meet the challenges imposed on software testing. In model-based testing a system under test (SUT) is tested against a formal description, or model, of the SUT’s behavior. Such a model serves as a precise and complete specification of what the SUT should do, and, consequently, is a good basis for testing. Moreover, such models can be automatically processed by tools, which make it possible to effectively automate the testing process. This lead to faster and less error-prone test generation: millions of test events can be automatically generated from the model, and subsequently executed and analyzed. And if the model is valid, i.e. expresses precisely what the SUT should do, then all these tests are also provably valid. This presentation will discuss model-based testing in general, and model-based testing for transition systems in particular.

The “ioco testing theory” for labeled transition systems is presented, including a test generation algorithm that is shown to produce provably sound and exhaustive test suites. Moreover, some variants of ioco, the consequences for compositional testing, and some tools for model-based testing will briefly be addressed.

Speaker Details

Jan Tretmans is researcher at the Embedded Systems Institute (ESI) in Eindhoven, and part-time associate professor at the Radboud University Nijmegen, both in The Netherlands. He is working in the areas of software testing, and the use of formal methods in software engineering; in particular, he likes to combine these two topics: testing based on formal specifications, also referred to as model-based testing. In this field he has several publications, and he has given numerous presentations at scientific conferences as well as for industrial audiences. Jan Tretmans holds a degree in Electrotechnical Engineering and a PhD in Computer Science, both from the University of Twente in The Netherlands. He spent some time as a post-doctoral researcher in Norway, Greece and Germany, and for a couple of years he was in involved in the academic-industrial transfer of formal methods technology. Before joining ESI he was at the University of Twente, and full-time at the Raboud University Nijmegen. Currently he is involved in the Dutch research projects Atomyste, Stress, and Tangram, and in the EU projects Tarot and Artist2, which all address some aspect of the theory, tools and applications of model-based testing based on formal methods, and in which industrial-academic collaboration plays an important role.