Formal Analysis of Timing Effects on Closed-loop Properties of Control Software

Abstract : The theories underlying control engineering and real-time systems engineering use idealized models that mutually abstract from central aspects of the other discipline. Control theory usually assumes jitter-free sampling and negligible (constant) input-output latencies, disregarding complex real-world timing effects. Real-time systems theory uses abstract performance models that neglect the functional behavior and derives worst-case situations with limited expressiveness for control functions, e.g., in physically dominated automotive systems. In this paper, we propose an approach that integrates state-of-the art timing models into functional analysis. We combine physical, control and timing models by representing them as a network of hybrid automata. Closed-loop properties can then be verified on this hybrid automata network by using standard model checkers for hybrid systems. Since the computational complexity is critical for model checking, we discuss abstract models of timing behavior that seem particularly suited for this type of analysis. The approach facilitates systematic co-engineering between both control and real-time disciplines, increasing design efficiency and confidence in the system. The approach is illustrated by analyzing an industrial example, the control software of an electro-mechanical braking system, with the hybrid model checker SpaceEx.
Type de document :
Communication dans un congrès
35th IEEE Real-Time Systems Symposium 2014 (RTSS), Dec 2014, Rome, Italy. 〈http://2014.rtss.org/〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01097622
Contributeur : Sophie Quinton <>
Soumis le : samedi 20 décembre 2014 - 11:17:07
Dernière modification le : lundi 5 octobre 2015 - 16:59:32

Identifiants

  • HAL Id : hal-01097622, version 1

Collections

Citation

Goran Frehse, Arne Hamann, Sophie Quinton, Matthias Wöhrle. Formal Analysis of Timing Effects on Closed-loop Properties of Control Software. 35th IEEE Real-Time Systems Symposium 2014 (RTSS), Dec 2014, Rome, Italy. 〈http://2014.rtss.org/〉. 〈hal-01097622〉

Partager

Métriques

Consultations de la notice

139