Monitoring and fault-diagnosis with digital clocks

Karine Altisen*, Franck Cassez, Stavros Tripakis

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contributionpeer-review

3 Citations (Scopus)

Abstract

We study the monitoring and fault-diagnosis problems for dense-time real-time systems, where observers (monitors and diagnosers) have access to digital rather than analog clocks. Analog clocks are infinitely-precise, thus, not implementable. We show how, given a specification modeled as a timed automaton and a timed automaton model of the digital clock, a sound and optimal (i.e., as precise as possible) digital-clock monitor can be synthesized. We also show how, given plant and digital clock modeled as timed automata, we can check existence of a digital-clock diagnoser and, if one exists, how to synthesize it. Finally, we consider the problem of existence of digital-clock diagnosers where the digital clock is unknown. We show that there are cases where a digital clock, no matter how precise, does not exist, even though the system is diagnosable with analog clocks. Finally, we provide a sufficient condition for digital-clock diagnosability.

Original languageEnglish
Title of host publicationProceedings
Subtitle of host publicationSixth International Conference on Application of Concurrency to System Design, ACSD 2006
Place of PublicationPiscataway, NJ
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
Pages101-110
Number of pages10
ISBN (Print)0769525563, 9780769525563
DOIs
Publication statusPublished - 2006
Externally publishedYes
Event6th International Conference on Application of Concurrency to System Design, ACSD 2006 - Turku, Finland
Duration: 28 Jun 200630 Jun 2006

Other

Other6th International Conference on Application of Concurrency to System Design, ACSD 2006
CountryFinland
CityTurku
Period28/06/0630/06/06

Fingerprint Dive into the research topics of 'Monitoring and fault-diagnosis with digital clocks'. Together they form a unique fingerprint.

Cite this