IST-2001-33522 OMEGA

Correct Development of Real-Time Embedded Systems

Welcome to the project homepage


Home
The OMEGA toolset
The OMEGA UML profile
Case studies
Publications and bibliography
Download documents
Partners & Persons
Dissemination
Related links


(Re-)Login
Untitled Document

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.

You are currently authenticated as omegapublic (level 0)
(Re-)Login
For comments about this site please contact the webmaster