Beskrivelse
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:
Real-Time Modeling Introduction to timed automata (TA) Real-Time Conformance Real-time extensions of the ioco testing theory Off-Line Testing Off-line generation of (optimal) quantitative test-sequences and testing strategies (based on Priced TA and Timed Games) On-Line Testing Online real-time testing and monitoring; Case study Future ChallengesUPPAAL 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.| Periode | 26 jun. 2007 |
|---|---|
| Begivenhedstitel | Fates/Testcom 2007 |
| Begivenhedstype | Konference |
| Placering | Talinn, EstlandVis på kort |