June 26-29 2007, Tallinn, Estonia

Back to the list of tutorials.

Model-Based Testing of Real-Time Systems

Brian Nielsen, University of Aalborg, Denmark

Brian Nielsen is associate professor at Department of Computer Science at Aalborg University, Denmark. He is working in the area of distributed and embedded systems, currently emphasizing automated formal model-based development and testing of real-time systems. In this field he has several publications, and he has given numerous presentations at scientific venues as well as for industrial audiences.
Brian Nielsen holds an MSc degree in electronic engineering and a PhD in computer science, both from Aalborg University. He has been a visiting researcher at the University of Illinois and University of Bremen. He is very active in the Centre of Embedded Software Systems (CISS) where he is managing several industrial collaboration projects in software testing and application of automated model-based testing. He is also active in the European ARTIST Network of Excellence, and other national and international research projects.

For many systems the timing of events is of utmost importance for their correctness and usability. Typical examples are embedded systems and control-systems. In such real-time systems, their actual quantitative timing properties is as important as the pure functionality.

Research in model-based testing has been progressed significantly during the last years, however, support for quantitative properties like real-time is still relatively immature.

In this tutorial we introduce recent advances in model-based testing of real-time systems, including models, theory, principles, techniques, and tools. Specifically, we introduce timed automata as means for modelling timing requirements, notions of real-time conformance, principles for off-line and on-line generation of real-time test cases, and using the Uppaal tool-suite for these tasks. Finally, we discuss the future challenges that remain. Contents:

  1. Real-Time Modeling
    • Introduction to timed automata (TA)
  2. Real-Time Conformance
    • Real-time extensions of the ioco testing theory
  3. Off-Line Testing
    • Off-line generation of (optimal) quantitative test-sequences and testing strategies (based on Priced TA and Timed Games)
  4. On-Line Testing
    • Online real-time testing and monitoring; Case study
  5. Future Challenges

UPPAAL is a tool for modelling, simulating and verifying real-time systems, developed as a collaboration between BRICS at Aalborg University and Department of Computer Systems at Uppsala University since the beginning of 1995.

UPPAAL Tron is a testing tool, based on the UPPAAL engine, allowing for on-line conformance testing of timed systems, mainly targeted for embedded software commonly found in various controllers. By on-line we mean that tests are derived, executed and checked simultaneously while maintaining the connection to the system in real-time.

UPPAAL Cora is a branch of UPPAAL targeted towards optimal scheduling and planning problems with numerous applications to embedded systems. The modelling formalism of UPPAAL Cora is that of priced timed automata - an extension of the classical timed automata model - allowing models to be annotated with information describing how various types of costs and rewards (e.g. energy, throughput) may accumulate during the behaviour of a model.

UPPAAL Tiga is the most recent branch of UPPAAL supporting controller synthesis for real time systems through the computation of winning strategies for timed games.

Both UPPAAL Cora and UPPAAL Tiga allow for efficient off-line generation of (cost-wise) optimal test-suites with guaranteed coverage.