Research and Integration Activities for the "Real Time Components" cluster

Platform for Component Modelling and Verification
JPIA-Platform


Artist2 Clusters:
- Real-Time Components

Activity Leader:
Susanne Graf (Verimag)
Abstract
Integrate the relevant European research on tools for modelling and analysis of component-based real-time systems by building tool supported semantic based platform for standard modelling notations that are relevant for the design of embedded systems.
These platforms will support transformations from modelling standards to semantic kernel languages to leverage associated powerful analysis tools, in particular some of those from the “Testing and Verification” cluster.

Participants

The full list of participants is available here.

Baseline

Before the beginning of ARTIST, UML began to be accepted as a standard for model-based development, also in the context of real-time and embedded systems, even if it was lacking a number of concepts needed for this purpose and supporting validation tools. In the context of real-time embedded systems, there existed a number of UML based CASE tools (e.g., Artisan, Rhapsody, RoseRT, TAU) and there exist also a large number of analysis and validation tools, mostly coming from academia. With a few exceptions, they were dedicated to specific profiles taking into account a small subset of UML and are weakly integrated in the development flow.

Several of the platform participants had already started considerable efforts for integrating analysis and validation into the development flow --- in particular in the framework of IST projects AIT-WOODES (CEA: Accord Methodology and tool support, OFFIS: verification tool for UML in Rhapsody), OMEGA (VERIMAG: IF verification tool for real-time UML, OFFIS: verification tool for UML), and Metropolis (PARADES: UML platform).

Previous Work

The main objective of the first year of the project was to obtain an inventory of potentially interesting tools, possibly to do some initial developments within these tools towards a possible integration, and finally, to define a concrete vision of the ARTIST platform for component-based design and validation. This has been done during the meetings held in Grenoble in October 2004, in Paris in January 2005 and in Rennes, at the end of June 2005. The June 2005 meeting has been hold in common with the hard real time and the adaptive real time clusters.

We had chosen the option to first connect a restricted set of model-based analysis and validation tools with the help of tools implementing UML compatible model transformation technology and possibly – if this turns out to be useful – tools allowing to generate complex functionalities from basic ones by means of abstract specifications. The set of participating tools is always to be considered preliminary; new tools were expected to join the platform over time.

Due to the large span of applications covered by the tools to be integrated into to the platform, this integration was not intended to be a strong integration in the classical sense of an integrated toolset, but rather a set of components that can be used in combination with specific components to form different tool chains. A baseline of the tools is that they are or will be made UML compatible. Some components are designed to be specific to particular tool-chains and whereas others are useful in several ones.

Presently considered tool chains used in case studies had been identified by the following working titles:
  • A platform for the analysis of safety-critical embedded systems. This platform was planned to be developed mainly in the context of the future OpenEmBeDD (started in 2006), CAROLL, ASSERT and SPEEDS (started in 2006), with contributions from SAVE and ASTEC.
  • A platform for the analysis of performance critical service-based systems. The Persiform project began developing this platform. The plan defined for the second year was to provide a mapping to a commercial performance analysis tool.
  • A platform for the certification of smart-card applications. This platform was planned to be developed mainly in the EDEN project and its successor EDEN-2.

The relevant subsets of UML used in the context of these three environments are specific to the concerned target application types. The first one will focus on system specifications, where the behaviour of individual components are specified by means of state-machines and requirements by state-machines and possibly Sequence diagram. This Profile will consist of the MARTE profile and the Rich Component concept to be developed in SPEEDS. The second platform will focus on early performance specifications described in terms of activity diagrams. It is being developed in the Persiform project. The main focus of the third is the expression of security properties which are developed in the EDEN projects.
The performance annotations in platform 2 will use a subset of the timing annotations in MARTE. For the description of design specifications in platforms 2 and 3 (considered in a later stage), it may be interesting to consider a subset of the profile of platform 1, but this has to be studied further. Also the profile concerning architecture modelling may be shared, but again, this will be considered later.

The analysis tools should in principle be sharable amongst the platforms thanks to the mapping into a semantic level model. Our initial focus is on the following tools Agatha (CEA) for scheduling analysis and test case generation, IF/BIP (VERIMAG) for simulation and verification of timed specifications, HERMES (VERIMAG) for the verification of secrecy properties, TIMES (Uppsala) and MAST (U. Cantabria) for scheduling analysis, OFFIS tools for model-checking, safety and fault analysis, and Metropolis (PARADES) for simulation, architectural design exploration and connection to external model-checkers like SPIN. There is some overlap in the functionalities of the validation tools, but they are based on different algorithms and have different strengths and weaknesses. Some new analysis methods, specific to the needs of the specific applications will be built.
The tool jETI (U. Dortmund) is intended for a high-level integration of tool functionalities. It allows the specification of complex functionalities from functionalities provided by different tools. This kind of user-level tool integration was totally absent in earlier projects and requested by users. This activity will not be the first priority in the near future, but it will be definitely considered.
An overview on the initial version of the targeted architecture, indicating both shared and specific parts are given in Fig. 1 above. The developed tools will be ported to Eclipse.

During the first year of ARTIST, we have done only a limited amount of integration. The main progress was on individual components for these platforms.

Current Results

1. Modelling languages and interaction with standards
The work on the platform interacts with and depends on several activities related to the development of UML-based modelling languages and the development of formalisms for a semantic level representation of models. An important goal is achieving tool chains for related profiles by mapping them to a small set of semantic level formalisms used in validation and code generation tool chains. This should finally allow handle models more than one profile simultaneously. This section presents both user-level and semantic-level formalisms. In fact, the separation between these levels is sometimes narrow, as user-level profile will lift some of the concepts useful for validation at the user level and in some cases may be used for both purposes. We start with those clearly meant as user level language and pass then to semantic level formalisms.

2. Platform for the analysis of safety critical embedded systems
The works carried out for this platform are building on UML profiles, in particular MARTE and HRC. The main efforts this year concern back-end tool chains, starting from one of the envisaged semantic level formats and integrating validation and code generation tools. The work on the front-end tools, providing mappings from user level profiles to semantic level formalisms has only started for MARTE and will start within the next year for HRC.

3. Platform for the analysis of performance critical systems
This platform is presently developed in the context of the French Persiform (http://www-persiform.imag.fr) project (with ARTIST partners FTRD, INRIA and VERIMAG). The aim of this project is the integration of performance evaluation and formal verification in requirement and design activities.
A first aim is to connect commercial performance analysis tool (event-based simulation mainly) to functional UML modelling tools for high-level performance analysis, in particular service specifications expressed in terms of activity diagrams [BCG*06] and sequence diagrams. For this purpose, a profile for the use of activity diagrams has been defined and a formal semantics has been through a mapping to a restricted class of coloured Petri nets plus annotations with probabilities and distribution concerning timing and resource usage. Annotated Petri nets are then transformed into performance evaluation platform SES Workbench (http://www.mmsolutions.com/english/...). Alternatively MSC can be handled a transformation into the same class of annotated Petri nets. These transformations are based on the construction of meta-models for the different languages and transformation rules.

4. Platform for the certification of smart-card applications
The work on this platform is supported by a collaboration between CEA and VERIMAG on functional validation of critical applications on smart cards. This work is carried out in the context of a national project, EDEN 2, that pursue the work done in the previous one, EDEN, in order to reach a consolidated implementation for industrial exploitation. It has not progressed exactly according to the plans which foresaw the definition of a UML profile for security properties, but it turned out to be more important to concentrate in the first year rather on the validation engine.

5. Generic validation technology for non functional properties and component systems
The development of new verification techniques is not the primary goal of the component platform; this topic is covered by the Verification cluster and platform activities and the background tools of the platform have been described in the year 1 deliverable. We describe here on some new developments directly linked to the connection of existing verification tools to the modelling languages considered in the platform.

An interesting technical challenge for adapting UPPAAL for asynchronous models is to check the boundedness of channels, and to synthesize the maximal size of memory blocks needed to implement the channels. Preliminary results are reported in [KY06] showing that the expressive power of such systems with two channels — that are no more expressive than finite-state machines in the untimed setting — is Turing-equivalent. We have been developing methods based on approximations. As an abstraction for communication interfaces, we have adopted arrival curves from network calculus. Some preliminary results are achieved, and they will be implemented in the coming versions of UPPAAL for verification of systems with asynchronous communication. The work will be extended and integrated in the TIMES tool [FMPY06] for approximate schedulability analysis of systems with multi-resource and heterogeneous components.

Keynotes, Workshops, Summer Schools, Tutorials

Keynote: "A Framework for Component-based Construction"
3rd IEEE International Conference on Software Engineering and Formal Methods (SEFM05)
Koblenz (D)– September 7-9, 2005
Joseph Sifakis (Verimag) presents the component framework BIP and plans for implementing it; which meanwhile has been achieved and will be used for connecting modelling and validation tools

Keynote: “Modelling Heterogeneous Real-time Components in BIP”
IEEE International Conference on Software Engineering and Formal Methods (SEFM06)
Pune, India – September 11-16, 2006
Josef Sifakis (VERIMAG) presented the BIP framework and its implementation focussing on case studies
See it online!

Keynote: "Modelling and verification of RTES: a framework & experimental results"
Workshop QAPL on quantitative aspects in programming languages at ETAPS 2006
Vienna (A)– April 2, 2006
Keynote talk by Susanne Graf (VERIMAG) on the modelling and validation problems encountered in the context of RTES, the modelling and IF-based validation framework implemented in OMEGA on hand of an industrial case study
See it online!

Keynote: ”UML and Components for System Modelling”
Conference name Euromicro – SEAA (Software Engineering and Advanced Applications) -
Porto, Portugal – August 30 – September 3, 2006
François Terrier (CEA) presented an overview of the component concepts proposed by the standard UML2, its relations with middleware related component concepts and their benefits in a Model Driven Engineering process.
See it online!

Workshop: MARTES 2005, Modelling and Analysis of Real Time and Embedded Systems
MoDELS/UML 2005, Int. Conf. on Model Driven Engineering Languages and Systems
Montego Bay, Jamaica, Oct. 4, 2005
VERIMAG and CEA have been the initiators of this workshop on model-driven development and real-time and embedded systems as a follow-up event on the successful workshop series on Real time embedded systems SIVOES and SVERTS. MARTES has been hold in October 2005 as a satellite event of the MoDELS conference. The workshop attracted a number of interesting submissions and participants. The results of the workshop, as well as 2 best papers have been published in an LNCS volume. See it online!

Presently, the second edition, to be held on October 3, 2006 in Genoa, Italy in conjunction with MoDELS/UML 2006 is being prepared.. Almost 40 participants are expected.

Workshop MoDeVa 2005: Model Design and Validation
MoDELS/UML 2005, Int. Conf. on Model Driven Engineering Languages and Systems
Montego Bay, Jamaica, Oct. 4, 2005
The second edition of this workshop has been organized conjointly by the IRISA Lab of the University of Rennes and the CEA (who is the initiator of this workshop). It was held in October 2005 as a one day satellite event of the MoDELS conference. Half of the duration of the workshop was dedicated to pre-selected papers presentations and the other part of the workshop was dedicated to active discussions on different topics. A summary of those discussions together with the two best papers of the workshop have been published in [1]. The third edition of MoDeVa will be a satellite event of MoDELS 2006.

Workshop: Requirements for Flexible Scheduling in Complex Embedded Systems
Massy (France) the 16th of June, 2006
This workshop was organized by Michael González, from the University of Cantabria and Thales. It represents a collaboration with the Adaptive Real Time Cluster. It was held in Massy (France) the 16th of June, 2006. J. Medina presented in this workshop "Notes on the RT components-based framework for FRESCOR: modelling, verification, and run-time support". This presentation dealt with a number of issues about the requirements for scheduling services in the component-based framework envisioned for the FRESCOR project.

Workshop: Safe-UML: Modellierung und Safty-Normen, workshop at the Safetronic 2006, Munich, Germany, November 2006.
This workshop is organized by OFFIS together with OPRAIL partners. The topics of this workshop are related to the use of UML within the development of safety critical systems, where the development process has to be compliant to safety standards. Within this workshop the OPRAIL partners will report on there experience with Safe-UML.
See it online!

Summer school: MDD for Distributed Real Time Embedded Systems
Brest, France – September 4-8, 2006
This summer school was co-organized by CEA. It is the third edition of a series of summer school which focuses on model-driven related issues in the context of real-time and embedded systems development. The main goal of this summer school series is to provide participants with the most up-to-date information needed to understand and apply MDE approaches to the development of distributed, real-time and embedded systems. For that purpose, we have gathered experts from a variety of research labs and industries to give seminars that provide insights into the ongoing research works and practical applications related to MDE for DRES
See it online!

Summer school: ARTIST Summer school on Component & Modelling, Testing & Verification, and Static Analysis of Embedded Systems
Nässlingen, Sweden, September 29 to October 2, 2005
This summer school included contributions from several ARTIST clusters, and in particular several tutorials by the platform partners on relevant topics, such as modelling languages (MARTE), tools (IF, Metropolis), modelling techniques (BIP, Metropolis) and model transformation techniques (Kermeta)
See it online!

Tutorial: The IF toolset
SDLforum 2005
Grimstad, Norway, June 20, 2005
Iulian Ober presented the IF tool, by focussing on case studies successfully carried out within the Omega project with the IF tool chain for validating UML specs; IF will be connected to the platform.
See it online!

 

 

ARTIST2 Participants: Expertise and Roles

  • Platform Leader: Susanne Graf (Verimag)
    Contributions of her team: Semantic level formalisms including general component composition, formal verification methods and tools, in particular the IF/BIP validation platform for real-time and embedded systems
  • Team Leader: Sebastien Gérard (CEA)
    Contributions of his team: UML Profile for Modelling and Analysis of Real-Time and Embedded Systems: MARTE profile, modelling for RT/E Systems, code generation, RT/E analysis such as WCET and schedulability analysis.
  • Team Leader: Jacques Pulou (France Telecom R&D)
    Contributions of his team: connection of performance analysis tools to UML case
    tools and the Fractal/Think platform.
  • Team Leader: Thierry Coupaye (France Telecom R&D)
    Contributions of his team: his team has developed the architecture description language Fractal and its implementation Think. Contribution to the platform in the collaboration with Verimag on the integration of validation tools through the translation from Think to BIP
  • Team Leader: Jean-Marc Jézéquel (INRIA)
    Contributions of his team: UML-based model transformation technology.
  • Team Leader: Noël Plouzou (INRIA)
    Contributions of his team: Model transformations and aspect orientation, tools.
  • Team Leader: Bernhard Josko (OFFIS)
    Contributions of his team: OFFIS toolset for modeling of embedded systems and validation
  • Team leader: Alberto Sangiovanni-Vincentelli (PARADES)
    Contributions of his team: Platform-Based Design, UML Platforms and the Metropolis framework.
  • Team Leader: Bengt Jonsson (Uppsala)
    Contributions of his team: Connection between modelling and verification tools, Times tool

Affiliated Participants: Expertise and Roles

  • Team Leader: Julio Medina (U. of Cantabria)
    Contributions of his team: Schedulability Analysis and Component-Based solutions inside the standardization effort for the UML Profile for Modelling and Analysis of Real-Time and Embedded Systems: MARTE (prospective standard of the OMG).
  • Team Leader: Martin Torngren (KTH)
    Contribution of his team: liaison with the control cluster, participation in the IST project ATTEST contributing to the platform Team Leader: David Lesens (EADS). Contributions of his team: Proposal of case studies concerning architecture modelling (integration of AADL and UML) and timing analysis in the ASSERT project. Participated in a common publication.
  • Team Leader: Bernhard Steffen (University Dortmund)
    Contributions of his team: tool integration platform jETI.

(c) Artist Consortium, All Rights Reserved - 2006, 2007, 2008, 2009

Réalisation Axome - Création de sites Internet