An Abstraction-Refinement Theory for the Analysis and Design of Real-Time Systems

作者：Kurtin Philip S^*; Bekooij Marco J G

来源：ACM Transactions on Embedded Computing Systems, 2017, 16(5s): 173.

DOI：10.1145/3126507

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.

• 出版日期2017-10