Description
These lectures will give provide a thorough tutorial of the tool UPPAAL and the newly emerged branches UPPAAL Tron, UPPAAL Cora and UPPAAL Tiga (see www.uppaal.com) and their application to the modelling, simulation, verification, testing, scheduling and controller synthesis for real time and embedded systems. 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. The modelling language of UPPAAL is based on the notion of timed automata by Alur and Dill (1990) allowing system behaviour to be described as a networks of timed automata extended with data variables which may be manipulated by a rich C-like programming language. UPPAAL includes a similator for inexpensive validation of behaviour and a verifier for model-checking wrt safetly, liveness and bounded liveness properties. The newly released UPPAAL 4.0 offers a number of improvements and extension, including symmetry reduction, user defined functions, priorities on processes and channels, new abstraction techniques, a factor 3 to 5 reduction in memory usage, fully searchable help system, implementation of generalized sweep line method, record types, quantifiers in expressions, undo and redo support, syntax highlighting, custom location and edge colors, documentation comments on models and better trace facilities. 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 Tron 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 allows for efficient off-line generation of (cost-wise) optimal test-suites with guaranteed coverage.| Period | 26 Jun 2006 |
|---|---|
| Event title | TAROT SUMMER SCHOOL 2006 |
| Event type | Conference |
| Location | Toledo, SpainShow on map |