Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadatas
Contributor : Sophie Quinton <>
Submitted on : Saturday, December 20, 2014 - 11:17:07 AM
Last modification on : Tuesday, December 8, 2020 - 10:02:02 AM


  • HAL Id : hal-01097622, version 1



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. ⟨hal-01097622⟩



Record views