Artist Summer school - Verification of UML models with IF

This course is hold in the context of the Artist Summer school taking place September 29 - October 2, 2005 in Naesslingem, Sweden.

Title: Verification of UML models with timing constraints with IF

Speaker: Susanne Graf

Abstract:
This talk will give an overview on the IF, an open validation platform for asynchronous timed systems such as telecommunication protocols or distributed embedded applications. The IF toolbox is built upon a specification language based on timed automata with urgency extended with discrete data variables, various communication primitives, dynamic process creation and destruction. This language includes most of the concepts allowing the direct representation of modeling and programming languages for distributed systems like SDL, UML or Java, as well as extensions allowing the expressions of timing properties.

Here, we will focus on the use of IF for the validation of real-time properties of UML models. A short overview on the considered UML profile and the mapping principles from UML to IF will be presented, as well as the way in which semantic variations of the profile are anticipated. Then the usefulness of the UML profile for modelling of real-time systems and their properties, and the use of the IF toolset for their validation will be demonstrated on hand of one or two case studies. In particular, we will show the use of the considered UML profile for the validation of deployment related propserties such as scheduling and timely access to a shered bus.

This talk is related to the talk on Component-based modeling of real-time systems (see the program ). Several of the concepts presented in this talk have been implemented in IF and have shown their usefulness for obtaining faithful and direct mappings of high-level modeling languages.

A list of related documents and links :

The slides: the technical slides as a single file: slides in pdf
Susanne Graf
Last modified: Sun Aug 21 11:51:21 MEST 2005