Formal Methods for Real Time Systems Automatic Verification & Validation

10-11-98


Click here to start


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

Author: CS