Model CheckingAutomatic Verification

Model Checker

UPPAAL

System Description

Timed Automata A

Requirement

Specification F

A sat F

Yes!

No!

Diagnostic Infomation

89

90

93

94

95

97

98

Timed Automata

Decidability

Epsilon

TAB

Regions

HyTech

Polyhedra

UPPAAL

Kronos

Zones, DBM

Compact Datastr

Compositionality

History

Previous slide

Next slide

Back to first slide

View graphic version