文档介绍：Formal Verification of UML Statecharts
with Real-Time Extensions
  ¡  
Alexandre David M. Oliver Moller¨ Wang Yi
¡
  Uppsala University BRICS Arhusª
¢¤£¥¢§¦©¨§£
©¨ ¥£¤¤ ¤ ¥¤ ¥ ¤¥ ¤ ¨¥¤
£
Outline:
1 UML, Statecharts, and Time
2 Semantics for Formal Verification
3 Verifying a Pacemaker with UPPAAL
NWPT’01 10 OCTOBER 2001 OLIVER MO¨ LLER: FORMAL VERIFICATION OF UML STATECHARTS WITH REAL-TIME EXTENSIONS 1
Unified Modeling Language (UML)
Born from unification of other methods (Booch, OMT, OOSE)
Different views of a system:
A) user view - use case diagrams
B) structural view - class diagrams
C) behavioral view - statecharts
D) environmental view - deployment diagrams
E) implementation view - component diagrams
An evolving standard: finished 2000
finished 2001
work in progress (4 RFP issued May/Sept)
NWPT’01 10 OCTOBER 2001 OLIVER MO¨ LLER: FORMAL VERIFICATION OF UML STATECHARTS WITH REAL-TIME EXTENSIONS 2
The Statechart Formalism
Features
hierarchical state machines
parallelism (on any level)
!
history
munication
powerful synchronization mechanisms
inter-level transitions
actions that are dependent on states
"$#&%('*)+"-,.'/"-0
actions on entry/exit
...
NWPT’01 10 OCTOBER 2001 OLIVER MO¨ LLER: FORMAL VERIFICATION OF UML STATECHARTS WITH REAL-TIME EXTENSIONS 3
Restricted Statechart Formalism
Current restricted features
hierarchical state machines ✔
parallelism (on any level) ✔
;
< history ✔
no munication
no sync states
no inter-level transitions
no actions that are dependent on states
no actions on entry/exit
132547638+1--: instead:
hand-shake style synchronization
shared variables
NWPT’01 10 OCTOBER 2001 OLIVER MO¨ LLER: FORMAL VERIFICATION OF UML STATECHARTS WITH REAL-TIME EXTENSIONS 4
Real-Time Extensions
Clocks
(timed) Guards
Invariants
NWPT’01 10 OCTOBER 2001 OLIVER MO¨ LLER: FORMAL VERIFICATION OF UML STATE