Anzeige
Erschienen in:
2005 | OriginalPaper | Buchkapitel
Timing Analysis of Distributed End-to-End Task Graphs with Model-Checking
verfasst von : Zonghua Gu
Erschienen in: Embedded and Ubiquitous Computing – EUC 2005
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Real-time embedded systems must satisfy system-level timing constraints between external sensor inputs and actuator outputs. Real-time scheduling theory can be used to verify that the system is schedulable, that is, no deadlines are missed, but that alone is not enough. Given that the system is schedulable, how to verify that it satisfies system-level end-to-end timing constraints, such as freshness, correlation and separation? To address this question, we adopt the approach of formal modeling and model-checking. Specifically, we use Timed Automata and the model-checker UPPAAL for verification purposes. We have developed generic modeling templates for a class of distributed task systems that can be used as input the the model-checker in order to verify system-level end-to-end timing constraints. We use an application example of distributed real-time control system to illustrate the utility of our approach.