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. © IFIP International Federation for Information Processing 2005.
CITATION STYLE
Gu, Z. (2005). Timing analysis of distributed end-to-end task graphs with model-checking. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3824 LNCS, pp. 214–223). https://doi.org/10.1007/11596356_24
Mendeley helps you to discover research relevant for your work.