A Framework to Analyse Synchronous Data-flow Specifications
-
Abstract:
Presence and absence of signals inside a reaction are inherent to the
synchronous paradigm, as well as clocks which are sets of instants that
indicate when a given condition is fulfilled over a sequence of reactions
(e.g. when a signal is present). Clocks are essential to capture the control
in data-flow specifications; more generally relations between clocks should
be analyzed to verify some properties, e.g. to detect inconsistencies in
specifications. These relations express particular safety properties many
of which can be verified without considering the dynamic of systems, by
means of a static abstraction. We propose a language CL to describe such
properties and prove it decidable. Model-checking is derived for Signal
programs, on the basis of a translation from the static abstraction of
Signal into CL. Links with existing models and abstractions for the analysis
of Signal programs are largely discussed.
-
Bibtex entry:
@TechReport{RRIrisaNebutPinchinat01,
author = {M. Nebut and S. Pinchinat},
title = {A Framework to Analyse Synchronous Data-flow Specifications},
institution = {Irisa},
year = {2001},
number = {1402},
month = {nov}
}
PS file
Mirabelle Nebut
Last
modified: Wed Jan 29 18:23:11 /etc/localtime 2003