O'Reilly logo

Communicating Embedded Systems: Software and Design by Olivier H. Roux, Claude Jard

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

Chapter 6

Tools for Model-Checking Timed Systems 1

6.1. Introduction

In this chapter, we present different tools for verification of timed systems. UPPAAL [LAR 97a, BEH 04b] is a tool for model-checking real-time systems developed jointly by Uppsala and Aalborg Universities. The first version of UPPAAL was released in 1995 [LAR 97a] and has been in constant development since then [BEN 98, AMN 01, BEH 01a, BEH 02, DAV 02, DAV 03, DAV 06]. It has been applied successfully to case studies ranging from communication protocol to multimedia applications [HAV 97, LON 97, DAR 97, BOW 98, HUN 00, IVE 00, DAV 00, LIN 01]. The tool is designed to verify systems that can be modeled as networks of timed automata [ALU 90a, ALU 90b, HEN 92, ALU 94] extended with integer variables, structured data types, user defined functions, and channel synchronization. Uppaal-CORA is a specialized version of UPPAAL that implements guided and minimal cost reachability algorithms [BEH 01b, BEH 01c, LAR 01]. It is suitable in particular to cost-optimal schedulability problems [BEH 05a, BEH 05b]. Uppaal-TIGA [BEH 07] is a specialization of UPPAAl designed to verify systems modeled as timed game automata where a controller plays against an environment. The tool synthesizes code represented as a strategy to reach control objectives [DEA 01, ASA 98, MAL 95, TRI 99]. The tool is based on a recent on-the-fly algorithm [CAS 05] and has already been applied to an industrial case study [JES 07]. The tool can also handle ...

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

Start Free Trial

No credit card required