Hierarchical Design and Analysis of Timed Systems

Project no: 9811-5

Wang Yi

Uppsala University, Informationtechnology

Application as pdf, ps , Complement to application as HTML, support letter 1 from Volvo Technological Development Corporation and support letter 2 from Mecel AB, ABB Automation Products.
Prolongation application 01-06-30 and support letter.

Support: 1 PhD student for 2 years decided 98-12-09.

Start 99-01-01 with Alexandre David as Phd student.

Reports: at ARTES RT-grad student day 99, progress page.
Updated project plan as pdf, ps.
1-year-report 00-06-06, second-year report 01-06-30

Local web: http://www.docs.uu.se/~yi/ARTES/UL/home.html

 

Industry contacts

Ulf Hammar ulf.h.hammar@se.abb.com

ABB Automation Products AB

Västerås

Project: Hierarchical Design and Analysis of Timed Systems

 

Lars Magnusson lars.magnusson@mecel.se

Mecel AB

Göteborg

Project 1: A tool environment for the development of embedded systems

Project 2: Identification of Complexity-Reduction Techniques for Optimal Scheduling in Embedded Distributed Real-Time Systems

Project 3: Hierarchical Design and Analysis of Timed Systems

Project 4: Flexible reliable timing constraints

Project 5: RATAD, Reliability And Timing Analysis of Distributed systems

Project 6: Extension of Project “Flexible Reliable Timing Constraints”

 

Ola Lundkvist ola.lundkvist@volvo.com

Volvo Technological Development Corporation

Dept 06200 CTP

Göteborg

Project: Hierarchical Design and Analysis of Timed Systems

 

Overview

A real-time system often contain a number of processes constituting a network. Many of the existing verification tools e.g. Kronos, HyTech and UPPAAL are designed to model the processes as a flat network and search through all the possible combinations of local states of the processes. This restricts the applicability of these tools to real-world systems that often contain hundreds or thousands of processes. It is in practice impossible for them to deal with such huge networks of processes due to the state-space explosion problem. A crucial observation is that the processes may be in many cases partitioned into classes. Processes in each of the classes may be analyzed separately from the other classes. The procedure may be continued within each class. This is the so-called hierarchical analysis. Unfortunately, there is few automatic verification tool supporting this type of analysis. We mention a few examples. SMV models a system e.g. a hardware circuit as a huge binary decision diagram with no structural information at all. The validation tool SDT for SDL only supports two-level hierarchy; but SDT is basically a simulation tool. Similarly STATEMATE based on state-charts supports hierarchical modelling and simulation to some extent; but no model-checker is available, in particular, for checking real-time properties.

Results

The first step of the project was planned to develop a modelling language to model and simulate hierarchical structures. A prototype (named UL++) is currently available. We plan to finalize the implementation of UL in Java and integrate it with the UPPAAL tool. Hopefully, in the short future, it will replace the current UPPAAL description language and user interface. We should point out that the UL project is naturally related to the existing code-generation project supported by ARTES as both address language design issues and more importantly the code-generation project is to generate runnable codes from design specifications written in UL. The future plan with the UL--project is to develop verification techniques that utilize the hierarchical information in order to guide the state--space exploration algorithm that the UPPAAL engine is based on and to introduce abstraction in the UPPAAL simulator and diagnostic trace--generator.

Co-operation

During 1999, there have been regular visits between ABB Automation Products (Ulf Hammar) and members of this project.

Publications

1. Tobias Amnell, Alexandre David, and Wang Yi. A Real Time Animator for Hybrid Systems. Tech Report, Department of IT, Uppsala University, March, 2000. To be included in the proceedings of 6th ACM SIGPLAN LCTES'2000.
2. Alexandre David, Practical Verification of Real-time Systems. Licentiate Theses from the Department of Information Technology, 2001-13 October 2001. ISSN 1404-5117.
3. A. David and M. O. Möller, From HUppaal to Uppaal A translation from hierarchical timed automata to flat timed automata. BRICS report RS-01-11, Dept. of. Computer Sci. Åhus Univ. Denmark 2001
4. David A., Oliver M. M. and Yi, W. Formal Verification of UML Statecharts with Real-Time Extensions. Department of Information Technology, Technical Reports ISSN 1404-3203.
5. Alexandre David and Wang Yi, Hierarchical Timed Automata for UPPAAL, Presented at The 10th Nordic Workshop on Programming Theory (NWPT'98), Turku Centre for Computer Science (TUCS), Finland, October 14-16th, 1998.
6. Alexandre David and Wang Yi, Modelling and Analysis of a Commercial Field Bus Protocol, Accepted for presentation at the 12th Euromicro Conference on Real Time Systems, Stockholm, June 19th-21st, 2000.