Communicating Embedded Systems: Software and Design

Chapter 6

Tools for Model-Checking Timed Systems ¹

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 ...