Validation of mixed SIGNAL-ALPHA Real-Time systems through affine calculus on clock synchronisation constraints

Abstract

In this paper we present the affine clock calculus as an extension of the formal verification techniques provided by the Signal language. A Signal program describes a system of clock synchronisation constraints the consistency of which is verified by compilation (clock calculus). Well-adapted in control-based system design, the clock calculus has to be extended in order to enable the validation of Signal-Alpha applications which usually contain important numerical calculations. The new affine clock calculus is based on the properties of affine relations induced between clocks by the refinement of Signal-Alpha specifications in a codesign context. Affine relations enable the derivation of a new set of synchronisability rules which represent conditions against which synchronisation constraints on clocks can be assessed. Properties of affine relations and synchronisability rules are derived in the semantical model of traces of Signal. A prototype implementing a subset of the synchro-nisability rules has been integrated in the Signal compiler and used for the validation of a video image coding application specified using Signal and Alpha.