International Workshop

SVERTS: Specification and Validation of UML models for Real Time and Embedded Systems

hold on

October, 11, 2004 in Lisbon, Portugal

in conjunction with

Seventh International Conference on the Unified Modeling Language, UML 2004"

[Home ] [Organizers] [Links] [Call for Papers]

List of accepted papers

  1. Comparing two UML profiles for non-functional requirement annotations: the SPT and QoS profiles
    Bernardi Simona, Dorina Petriu
    Paper Type: research  #1
    Abstract: The paper compares two UML Profiles adopted by OMG for annotating non-functional requirements of software systems: the UML Profile for Schedulability, Performance and Time (SPT) formally adopted in 2003 and the recently emerging UML Profile for Modeling Quality of Service and Fault Tolerance Characteristics and Mechanisms (QoS). The SPT Profile was the first attempt to extend UML with basic timing and concurrency concepts, and to express requirements and properties needed for conducting schedulability and performance analysis.
    While the SPT Profile is focused on these two types of analysis, the more recent QoS Profile has a broader scope, aiming to allow the user to define a wider variety of QoS requirements and properties. In order to compare the two profiles, we will focus on performability and timing aspects of software systems, by exemplifying the concepts through an example of embedded automation system. The comparative analysis shows that new concepts are needed in both profiles to express time intervals between two arbitrary events. Also, the two profiles will need to reach a common agreement on the specification of complex timing values, especially of those with stochastic characteristics. Another open problem is the parameterization of models, as in many cases fixed values for model parameters are not enough. The SPT Profile goes a step further by supporting symbolic variables and expressions, but the QoS Profile does not have such a capability yet. In general, both Profiles struggle with the balance between flexibility (i.e., allow the user to introduce its own definitions) and simplicity/convenience of expression.
    The challenge when defining a UML profile is to find convenient yet powerful mechanisms of expression for complex concepts, yet to remain within the limits of the UML standard extension mechanisms, which is necessary to insure that the annotated models could be understood by standard UML tool.
    Keywords, subject of the call: modelling real-time aspects in UML (SPT and QoS profile

  2. Real-Time Requirements in Formalized Use Cases: Specification and Validation
    Risto Pitkänen and Tommi Mikkonen
    Paper Type: research #3
    Abstract: The design of software systems usually advances from abstract to more concerete. Unfortunately, proper specification of real-time related issues has often been postponed to the implementation phase, potentially leading to increased complexity in design. This has at least partly been due to the lack of suitable abstractions and notations for expressing real-time requirements at an abstract level, using e.g. use cases. In this paper, we introduce an approach, where use-case level behavioral specifications can be augmented with real-time properties.
    We also show that these properties can be treated as a separate issue from the underlying behavior for e.g. eased reasoning. In addition, we will briefly discuss the verification and validation of such specifications from the viewpoint of automated tool support.
    Keywords, subject of the call: modelling and validation of real-time aspects

  3. Incremental Design and Formal Verification with UML/RT in the FUJABA Real-Time Tool Suite
    Sven Burmester, Holger Giese, Martin Hirsch, and Daniela Schilling
    Paper Type: research  #9
    Abstract:Model checking of complex time extended UML (UML/RT) models is limited today due to two main obstacles: (1) The state explosion problem restricts the size of the UML/RT models which can be addressed and (2) standard model checking approaches cannot be smoothly integrated into the usually incremental and iterative design process. The presented solution for incremental design and verification with UML/RT within the FUJABA Real-Time Tool Suite overcomes these two obstacles by applying a compositional reasoning approach [1] that is based on a restricted notion of UML patterns and components.
    A mapping of a subset of the UML/RT component model and additional real-time extensions for UML state diagrams to HUppaal enables the automatic, compositional formal verification of partial models such as patterns and components by means of a model checking PlugIn [2]. This tool support makes an incremental and iterative design and verification process possible where only the patterns and components which have been modified have to be rechecked rather than the whole UML/RT model.
    Keywords, subject of the call:  modeling of real-time aspects, timed automata based compositional validation

  4. A Formal Framework for UML Modelling with Timed Constraints: Application to Railway Control Systems
    Rafael Marcano, Samuel Colin and Georges Mariano
    Paper Type: research  #10
    Abstract: In the context of railway signalling systems, time related features play a relevant role at the validation process and specialists are more and more confronted with the necessity of applying formal methods as mean of preventing software faults. UML offers a standard notation for high quality systems modelling, however its current lack of formal semantics explains the existence of few tools supporting analysis and verification. In this paper, we propose a formal support of UML model-based verification using time-extended B specifications. The main goal is to enable consistency checking through UML diagrams using existing tools for B. A level crossing control system is developed in order to illustrate the approach.
    Keywords, subject of the call: modelling and validation  of reactive systems with UML and B

  5. An Analysis Tool for UML SPT Models
    John Hakansson, Leonid Mokrushin, and Paul Pettersson
    Paper Type: short tool paper  #15
    Abstract: In this paper we describe a plugin for the Rhapsody tool, which demonstrates how UML models with SPT tags can be analysed in the Times tool | a tool for modelling, schedulability analysis, and model-checking of task extended timed automata. The plugin converts a Rhapsody UML model consisting of components with their behaviours described as SPT annotated statecharts into a model that can be further analysed in the Times tool.
    In UML we use stereotype SAAction to annotate the operations of a statechart with timing paramters for their worst-case execution time, (relative) deadline, and priority. Using this information and the statecharts describing the behaviour of a component, we map the UML model into a set of tasks modeling the operations, and timed automata modelling the synchronous task release pattern speci ed by the statecharts. The development of the tool is still in progress and the input language is quite restricted. However, we have been able to successfully apply it to a Rhapsody model of an adaptive cruise controller.

  6. Validating UML models of Embedded Systems by Coupling Tools
    J. Hooman, Nataliya Mulyar, Ladislau Posta
    Paper Type: short  research paper  #18
    Abstract: The aim of this work is to support the multidisciplinary development of real-time embedded systems by combining tools of different disciplines. As a concrete example, we have coupled a UML-based CASE tool (Rose RealTime) and Simulink to allow simultaneous simulation. Since Rose RealTime does not have a well-defined notion of timed simulation, we have used the simulation time of Simulink also for Rose RealTime. An intermediate component has been implemented, which realizes time synchronization and data exchange between the tools.
    Keywords: Embedded systems; model-based development; simulation; real-time; UML; Simulink

  7. Worst-Case Execution Time Analysis from UML-based RT/E Applications
    Chokri Mraidha, Sébastien Gérard, François Terrier, David Lugato
    Paper Type: research paper #19
    Abstract: Moving from code-centric to model-centric development seems to be a promising way to cope with the increasing complexity of real-time embedded systems (RT/ES). These systems have various critical requirements that must be validated. Validation is then one of the key-point of their development. Relating to this goal, schedulability analysis methods are usually used to validate the system’s real-time requirements. Most of these methods rely on the knowledge of the Worst-Case Execution Time (WCET) of every task of the system. This paper presents an approach to derive WCET estimates for an application’s UML model.
    Keywords: Embedded systems; model-based development; simulation; real-time; UML; Simulink
    Keywords, subject of the call:: model level WCET computation of tasks for use in scheduling analysis