Artist Summer school - Verification of UML models with IF

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 :

• There are the presented slides


• The webpage of the IF verification platform containing links to manuals, downloadable code, case studies and contains also a tutorial.
  Below a few papers on the IF language and tool and the theory behind:
  • The paper presented at CAV 2002 explains the difference to the older versions of the language and the tool
  • The paper presented at SFM summer school 2004 gives a complete overview on the IF language and the tool architecture.
  • This paper which has been published in Information and Computation introduces timed automata with urgency which are the version of timed automata used in IF
  • This paper which has been presented at the Symposium FMCO 2003 shows the expressive power of priorities. Indeed, priorities have been very helpful for the mapping of different high level formalisms to IF.


• The webpage of the Omega project in which the considered UML profile and the UML interface IFx for IF have been developed.
  Below a few papers on the UML profile, in particular the real-time extensions and the work in connection with the IF tool. Overviews on all work done in Omega can be found on the Omega home page.
  • This paper which is being published in STTT gives an overview on the mapping from UML to IF, the IFx frontend and one of the case studies
  • This paper which is being published in STTT explains in details the real-time extensions of the UML profile.
  • This paper presents a case study carried out in the context of the Omega project and is to be presented at the MARTES workshop. Another case study is in this paper, and the Omega web page gives an overview on all case studies