Paper Info
Title
A New UML Profile for Real-Time System Formal Design and Validation
Abstract
UML solutions in competition on the real-time system market share three common drawbacks: an incomplete formal semantics, temporal operators with limited expression and analysis power, and implementation-oriented tools with limited verification capabilities. To overcome these limitations, the paper proposes a UML profile designed with real-time system validation in mind. Extended class diagrams with associations attributed by composition operators give an explicit semantics to associations between classes. Enhanced activity diagrams with a deterministic delay, a non deterministic delay and a timelimited offering make it possible to work with temporal intervals in lieu of timers with fixed duration. The UML profile is given a precise semantics via its translation into the Formal Description Technique RT-LOTOS. A RT-LOTOS validation tool generates simulation chronograms and reachability graphs for RT-LOTOS specifications derived from UML class and activity diagrams. A coffee machine serves as example. The proposed profile is under evaluation on a satellite-based software reconfiguration system.
Year
DOI
Venue
2001
10.1007/3-540-45441-1_22
Uml
Keywords
Field
DocType
formal description technique rt-lotos,precise semantics,uml class,uml profile,new uml profile,proposed profile,incomplete formal semantics,rt-lotos specification,explicit semantics,real-time system formal design,rt-lotos validation tool,uml solution,formal semantics,market share,activity diagram,composition operator,class diagram,real time systems
Programming language,UML tool,Unified Modeling Language,Computer science,Activity diagram,Reachability,Applications of UML,Semantics,Class diagram,Formal verification
Conference
ISBN
Citations 
PageRank 
3-540-42667-1
10
1.14
References 
Authors
12
5
Name
Order
Citations
PageRank
L. Apvrille1182.59
Pierre de Saqui-Sannes213318.91
Christophe Lohr3357.00
Patrick Sénac422222.89
Jean-Pierre Courtiat521632.68