| 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 |
| 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 |
| 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 |
| 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 |
| 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. |
| 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 |
| 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 |