Verifying quantitative real-time properties of synchronous programs

Abstract

We propose to apply the verification techniques available for Timed Graphs [ACD90], and particularly the symbolic model-checking algorithm of [HNSY92], to the Argos [Mar92] synchronous language. We extend the language with a single delay construct that allows to express watchdogs and timeouts, at any level in the parallel or hierarchic structure of a program. We define the semantics of this extended language in terms of Timed Graphs, and show that it is a “convenient” extension of the pure Argos synchronous semantics. Indeed, for discrete time, the two semantics coincide. The Timed Graph semantics can be viewed as a continuous time semantics for Argos. We extend the Argos compiler and connect it to the KRONOS tool which implements the abovementioned model-checking algorithm.