A Decidable Clock Language for Synchronous Specifications

Presence and absence of signals inside a reaction are inherent to the synchronous paradigm. Clocks are sets of instants (indicating for example when a signal is present) mainly used to describe the control part of data-flow specifications. The language C we define here expresses relations between cl...

Full description

Saved in:
Bibliographic Details
Published in:Electronic notes in theoretical computer science 2002-07, Vol.65 (5), p.125-139
Main Authors: Nebut, Mirabelle, Pinchinat, Sophie
Format: Article
Language:English
Subjects:
absence
abstraction
clock
decision procedure
model-checking
safety property
synchronous data-flow languages
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Presence and absence of signals inside a reaction are inherent to the synchronous paradigm. Clocks are sets of instants (indicating for example when a signal is present) mainly used to describe the control part of data-flow specifications. The language C we define here expresses relations between clocks. Such relations can describe the combinational part of specifications, as well as particular instantaneous safety properties. We give a decision procedure for C and apply it to the model-checking of Signal programs abstracted from their state handling part. Thanks to the use of clocks, absence is not explicitly encoded by a special value.
ISSN:1571-0661
1571-0661
DOI:10.1016/S1571-0661(05)80447-5