Aim of Omega
|
Definition
of a development methodology in UML for embedded and real-time systems
based on formal techniques
|
|
Approach
|
1.
Select a suitable subset of UML, adapted and extended
where needed with a special emphasis on time related aspects
The chosen subset includes: Class Diagrams and State Machines; Object Constraint
Language (OCL); Component descriptions including provided and required interfaces;
Use Case Diagrams, Live Sequence charts (an extension of UML's sequence
diagrams)
UML 2: we anticipate interesting features of the forthcoming
UML 2.0 standard, in particular, Architecture diagrams with ports
and connectors; Deployment Diagrams
Time extensions: based on the adopted profile for Schedulability,
Time and Performence. Includes special data types for time
and duration, a predefined package
defining timer and clock.
A rich set of predefined events
(which include a time stamp) and duration expressions;
the possibility to define time constraints on predefined or user defined
events and durations using OCL like syntax. Duration constraints based on event
observations can be defined using Omega observer
state machines
|
|
2.
Propose a development methodology, based on the
UML modeling and specification capabilities and the verification methods
and tools developed in the project.
Starting point: simple iterative, incremental
development process.
Activities for particular System Under Development, typically real-time
embedded system:
1. Requirements specification
and analysis
2. System analysis,
definition of architecture
3. Iterate following steps, for increasing part
of the System:
3.1
Analysis and design of parts
3.2
Refinement until it is close to concrete implementation
3.3
Implementation of (next) version on concrete platform (ultimate goal: generate
the implementation from the model)
|
| Workflow |
Omega / UML concepts |
Omega Tool support |
| Requirements |
Use Case Diagrams
Live Sequence Diagrams (LSC)
OCL
State Machines / Observers |
Editing and simulation of LSC
Consistency checks for LSC and OCL
Deduction of properties from given properties
|
| Architecture |
Components, Connectors, Ports, Required & Provided
Interfaces, OCL constraints, (Protocol) State Machines |
Correctness wrt requirements
Compositional verification
Timing Analysis |
| Analysis & Design |
Class Diagrams, OCL, State Machines |
Correctness wrt component specs
Synthesis of state diagrams
Correctness of refinement steps, within and between iterations |
| Platform dependent model |
Deployment Information (resources, scheduling policies,
execution time contraints |
Timing verification and synthesis of constraints |
|
|
3.
Provide formal foundations, methods and tools for
formal specifications and verification of real-time systems within UML
|
Specify interpretation for semantic variation points:
- Activity group: active object and a set of associated inactive objects
- one thread of control and signal queue
- run-to-completion semantics: event processing only in stable
states
- No shared variables between activity group
Both constraint and unconstraint interpretation of time progress
|
4.
Proposed methodology and tool-set evaluated on
four industrial case studies
|
| 5.
Dissemination: organisation of events and active
participation in UML 2.0 proposals |
Use the navigation links on the left to explore our pages. |
Don't forget to visit the IST
homepage. |
Home