The DisCo Home Page

Example: Verifying a real-time DisCo specification using Kronos

This page describes an example of verifying a real-time DisCo specification using the model-checking tool Kronos.

We have presented a mapping from instantiations of real-time DisCo specifications into timed automata. Kronos can be used to verify safety and bounded liveness properties of the automata. The mapping is described in the following paper:

Timo Aaltonen, Mika Katara, and Risto Pitkänen. Verifying Real-Time Joint Action Specifications Using Timed Automata. In Yulin Feng, David Notkin, and Marie-Claude Gaudel, editors, 16th World Computer Congress 2000, Proceedings of Conference on Software: Theory and Practice, pages 516-525, Beijing, China, August 2000. Publishing House of Electronics Industry and International Federation for Information Processing. IFIP.

The mapping is illustrated in the Figure below:

Generalized Railroad Crossing is a well-known benchmark problem for real-time specification and verification methods. The problem is to develop a system that operates a gate at a railroad crossing. The system should satisfy safety and utility properties, informally: the gate is down when there is a train in the crossing, and the gate is up when no train is in the crossing.

DisCo Specification

• Generic DisCo Specification

As a result of applying the mapping procedure to the two-train instantiation of the specification, we obtain 14 timed automata. Four of these correspond to DisCo objects (two Trains, one Gate, and one Controller), and ten to time variables of the specification (one automaton per variable).

Timed Automata

First Train

• train1
• train1_approach_ot
• train1_exit_dl
• product automaton

Second Train

• train2
• train2_approach_ot
• train2_exit_dl
• product automaton

Gate

• gate
• down_dl
• raise_ot
• up_dl
• product automaton

Controller

• controller
• approach_first_ot
• lower_dl
• raise_dl
• product automaton

Exit Timer

• exit_timer

Generalized Railroad Crossing (two trains, gate, controller and exit timer)

• product automata

The correctness criteria are expressed in the TCTL logic. We have verified four properties.

Verified Properties

• unreachability of error states
• non-zenoness
• safety
• utility

People involved in the study are Timo Aaltonen, Mika Katara and Risto Pitkänen.