Table of Contents
Formal Methods for Real Time Systems Automatic Verification & Validation
Outline
INTRODUCTION
Kim Guldstrand Larsen
Projects
UPPAAL?
Collaborators
Hybrid & Real Time Systems
Intelligent Light Control
Intelligent Light Control
Fischer’s Protocol A simple MUTEX Algorithm
Fischer’s Protocol A simple MUTEX Algorithm Adding Time
The Soldiers Problem Real time scheduling
Train Simulator
Model Checking Automatic Verification
Design Criteria
Modelling TIMED AUTOMATA
Timed Automata Finite Automata
Timed Automata
PPT Slide
PPT Slide
Various types of Clocks
Integrators
Networks of Timed Automata
Networks of Timed Automata
Exercise Sorting of Lego Boxes
Specifying Reachability & Beyond
Logical Formulas
Beyound Safety Decoration
Beyond Safety Test automata
DEMO
Overview of UPPAAL
Gear Controller with MECEL AB
THE UPPAAL ENGINE
Zones From infinite to finite
Symbolic Transitions
Forward Rechability
Forward Rechability
Forward Rechability
Forward Rechability
Compact Dastructures for Zones Difference Bounded Matrices
Compact Dastructures for Zones Difference Bounded Matrices
Compact Dastructures for Zones Difference Bounded Matrices
Improved Datastructures Compact Datastructure for Zones
Shortest Path Reduction 1st attempt
Shortest Path Reduction Solution
Shortest Path Reduction Solution
Shortest Path Reduction Solution
Reductions
CASE STUDIES
Audio & Video Components A line of industrial Real Time case studies
Audio & Video Components (cont.) Philips Protocol
Audio & Video Components (cont.) Bang & Olufsen IR Link, 1996-97
Audio & Video Components (cont.) Bang & Olufsen IR Link, 1996-97
Bang & Olufsen Power Down Module (1997)
More Industrial Case Studies
New Generations of UPPAAL STTT Workshop 1998
|