UML and RT-LOTOS: An integration for real-time system validation

Pierre De Saqui-Sannes; Ludovic Apvrille; Christophe Lohr; Patrick Sénac; Jean Pierrre Courtiat

UML and RT-LOTOS: An integration for real-time system validation

Pierre De Saqui-Sannes, Ludovic Apvrille, Christophe Lohr, Patrick Sénac, Jean Pierrre Courtiat

Research output: Contribution to journal › Article › peer-review

Abstract

The paper presents a UML profile that overcomes the limitations of real-time solutions currently available on the market. Associations between classes are given a formal semantics. New temporal operators are introduced; they include a non deterministic delay and a time-limited offering. UML models can be validated against logical and timing constraints. The profile's semantics is given through a translation into the formal language RT-LOTOS. The latter is supported by a validation tool which generates reachability graphs from extended UML models. A coffee machine serves as example in the paper. The profile is under evaluation on a satellite-based software reconfiguration system.

Original language	English
Pages (from-to)	1029-1042
Number of pages	14
Journal	Journal Europeen des Systemes Automatises
Volume	36
Issue number	7
Publication status	Published - 1 Dec 2002
Externally published	Yes

Keywords

Formal methods
RT-LOTOS
Real-time systems
UML
Validation

Cite this

@article{1b69355026bb412ba12edd32e5675d6d,

title = "UML and RT-LOTOS: An integration for real-time system validation",

abstract = "The paper presents a UML profile that overcomes the limitations of real-time solutions currently available on the market. Associations between classes are given a formal semantics. New temporal operators are introduced; they include a non deterministic delay and a time-limited offering. UML models can be validated against logical and timing constraints. The profile's semantics is given through a translation into the formal language RT-LOTOS. The latter is supported by a validation tool which generates reachability graphs from extended UML models. A coffee machine serves as example in the paper. The profile is under evaluation on a satellite-based software reconfiguration system.",

keywords = "Formal methods, RT-LOTOS, Real-time systems, UML, Validation",

author = "\{De Saqui-Sannes\}, Pierre and Ludovic Apvrille and Christophe Lohr and Patrick S{\'e}nac and Courtiat, \{Jean Pierrre\}",

year = "2002",

month = dec,

day = "1",

language = "English",

volume = "36",

pages = "1029--1042",

journal = "Journal Europeen des Systemes Automatises",

issn = "1269-6935",

number = "7",

}

TY - JOUR

T1 - UML and RT-LOTOS

T2 - An integration for real-time system validation

AU - De Saqui-Sannes, Pierre

AU - Apvrille, Ludovic

AU - Lohr, Christophe

AU - Sénac, Patrick

AU - Courtiat, Jean Pierrre

PY - 2002/12/1

Y1 - 2002/12/1

N2 - The paper presents a UML profile that overcomes the limitations of real-time solutions currently available on the market. Associations between classes are given a formal semantics. New temporal operators are introduced; they include a non deterministic delay and a time-limited offering. UML models can be validated against logical and timing constraints. The profile's semantics is given through a translation into the formal language RT-LOTOS. The latter is supported by a validation tool which generates reachability graphs from extended UML models. A coffee machine serves as example in the paper. The profile is under evaluation on a satellite-based software reconfiguration system.

AB - The paper presents a UML profile that overcomes the limitations of real-time solutions currently available on the market. Associations between classes are given a formal semantics. New temporal operators are introduced; they include a non deterministic delay and a time-limited offering. UML models can be validated against logical and timing constraints. The profile's semantics is given through a translation into the formal language RT-LOTOS. The latter is supported by a validation tool which generates reachability graphs from extended UML models. A coffee machine serves as example in the paper. The profile is under evaluation on a satellite-based software reconfiguration system.

KW - Formal methods

KW - RT-LOTOS

KW - Real-time systems

KW - UML

KW - Validation

M3 - Article

AN - SCOPUS:36448934908

SN - 1269-6935

VL - 36

SP - 1029

EP - 1042

JO - Journal Europeen des Systemes Automatises

JF - Journal Europeen des Systemes Automatises

IS - 7

ER -

UML and RT-LOTOS: An integration for real-time system validation

Abstract

Keywords

Fingerprint

Cite this