Formal Analysis of Timing Effects on Closed-loop Properties of Control Software - Archive ouverte HAL Access content directly
Conference Papers Year :

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

(1) , (2) , (3) , (2)
1
2
3
Goran Frehse
Arne Hamann
  • Function : Author

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.
Not file

Dates and versions

hal-01097622 , version 1 (20-12-2014)

Identifiers

  • HAL Id : hal-01097622 , version 1

Cite

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⟩
286 View
0 Download

Share

Gmail Facebook Twitter LinkedIn More