June 28, 2006 to June 30, 2006
Karine Altisen , Verimag Laboratory
Franck Cassez , IRCCyN Laboratory
Stavros Tripakis , Verimag Laboratory and Cadence Berkeley Labs
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ACSD.2006.10
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.
Karine Altisen, Franck Cassez, Stavros Tripakis, "In this work, we propose two translations: one from extended", ACSD, 2006, Sixth International Conference on Application of Concurrency to System Design, Sixth International Conference on Application of Concurrency to System Design 2006, pp. 101-110, doi:10.1109/ACSD.2006.10