Revisiting Timed Specification Theories: A Linear-Time Perspective
Revisiting Timed Specification Theories: A Linear-Time Perspective
复制标题
重新审视定时规范理论：线性时间视角
DOI：
10.1007/978-3-642-33365-1_7
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
Xu Wang
中科院分区：
文献类型：
--
作者：
Chris Chilton;M. Kwiatkowska;Xu Wang
我们认为，基于组件的实时系统的设计与关键的时间约束的设置。基于我们以前的工作，我们提出了一个组合规格理论的时间自动机与I/O的区别，它支持替代细化。我们的理论提供了操作的并行组合组成组件在运行时，逻辑合取/析取独立开发，和商增量合成。我们的时间理论的关键新奇在于最弱的同余保持安全性以及有界活性属性。我们发现，可以通过两个线性时间语义，定时跟踪和定时策略，其中后者是来自基于游戏的解释定时互动的一致性。
We consider the setting of component-based design for real-time systems with critical timing constraints. Based on our earlier work, we propose a compositional specification theory for timed automata with I/O distinction, which supports substitutive refinement. Our theory provides the operations of parallel composition for composing components at run-time, logical conjunction/disjunction for independent development, and quotient for incremental synthesis. The key novelty of our timed theory lies in a weakest congruence preserving safety as well as bounded liveness properties. We show that the congruence can be characterised by two linear-time semantics, timed-traces and timed-strategies, the latter of which is derived from a game-based interpretation of timed interaction.