Specification and Transformation of Reactive Systems with Time Restrictions and Concurrency

Specification and Transformation of Reactive Systems with Time Restrictions and Concurrency
复制标题

具有时间限制和并发性的反应式系统的规范和改造

DOI:
--
复制
发表时间:
1994
期刊:
Formal Techniques in Real-Time and Fault-Tolerant Systems
影响因子:
--
通讯作者:
M. Schenke
M. Schenke
中科院分区:
--
文献类型:
--
作者:
M. Schenke

文献摘要

被引文献

相似文献

本文介绍了一种方法中最困难的步骤,即如何将工期演算(DC)中的要求转换成occam程序,从而使其在构造上实现正确。将显示从DC到重要中间阶段(规范语言SLtime)的正确转换的几个规则。特别地,我们将解释需求和控制程序之间的相互作用,并行性的引入,以及从基于状态的dc描述到基于事件的sltime描述的变化。
In this paper the most difficult step of a method is presented by which requirements in the duration calculus (DC) can be transformed into occam programs such that the implementation is correct by construction. Several rules for correct transformations from DC towards an important intermediate stage, the specification language SLtime, will be shown. In particular we shall explain the interplay between requirements and a control program, the introduction of parallelism and the change from the state based DC-description to the event based SLtimedescription.