Meeting Deadlines Together (pdf)

by Laura Bocchi, Julien Lange, and Nobuko Yoshida

This paper studies safety, progress, and non-zeno properties of Communicating Timed Automata (CTAs), which are timed automata (TA) extended with unbounded communication channels, and presents a procedure to build timed global specifications from systems of CTAs. We define safety and progress properties for CTAs by extending the properties studied in communicating finite-state machines to the timed setting. We then study non-zenoness for CTAs; our aim is to prevent scenarios in which the participants have to execute an infinite number of actions in a finite amount of time. We propose sound and decidable conditions for these properties, and demonstrate the practicality of our approach with an implementation and experimental evaluations of our theory.

Full Version

The full version of the paper (with all proofs) is available here.

Benchmark Protocols

Graphical representations are available here (produced by the tool), textual inputs are together with the source code, see below.

Verification and Construction Tool

You may retrieve the source code by cloning our git repository:

run git clone -b cta --single-branch http://bitbucket.org/julien-lange/gmc-synthesis,
install and configure the dependencies listed in ./gmc-synthesis/README,
compile the tool (cf README),
./rungmc.py <path-to-ctas> runs the tool for a selected example (see tests/cta folder, e.g., ./rungmc.py tests/cta/benchmarks/ok/runningexample will run the tool on the running example in the paper).

The graphical outputs (.svg files) generated by the tool will appear in the ./gmc-synthesis/outputs folder.

The tool has been tested on Ubuntu 13.04 (Raring) and Mac OS X 10.9.5.