An Abstraction-Refinement Theory for the Analysis and Design of Real-Time Systems (Extended Version)

Component-based and model-based reasonings are key concepts to address the increasing complexity of real-time systems. Bounding abstraction theories allow to create efficiently analyzable models that can be used to give temporal or functional guarantees on non-deterministic and non-monotone implementations. Likewise, bounding refinement theories allow to create implementations that adhere to temporal or functional properties of specification models. For systems in which jitter plays a major role, both best-case and worst-case bounding models are needed. In this paper we present a bounding abstraction-refinement theory for real-time systems. Compared to the state-of-the-art TETB refinement theory, our theory is less restrictive with respect to the automatic lifting of properties from component to graph level and does not only support temporal worst-case refinement, but evenhandedly temporal and functional, best-case and worst-case abstraction and refinement. Compared to the journal version of this paper, we further present several additions in this extended version, such as an inclusion abstraction-refinement theory for the same component model, the definition of the expression of several timed dataflow models in our component model, as well as various formalizations of previously informal definitions and proofs