Deriving real-time action systems with multiple time bands using algebraic reasoning
Deriving real-time action systems with multiple time bands using algebraic reasoning
复制标题
使用代数推理导出具有多个时间段的实时动作系统
DOI：
10.1016/j.scico.2013.08.009
复制
发表时间：
2014
影响因子：
1.3
通讯作者：
Dongol B
中科院分区：
文献类型：
--
作者：
Dongol B
在开发的同时验证范式允许人们使用一系列针对剩余证明义务的计算，从它们的规范中增量地开发程序。本文提出了一种具有实际行为约束的实时系统的推导方法。我们开发了一个高级的基于区间的逻辑，它在实现中提供了灵活性，但允许对多个粒度进行代数推理，并对多个传感器进行延迟采样。用区间谓词和代数算子给出了动作系统的语义，统一了动作系统的逻辑及其性质，从而简化了计算和推导。
The verify-while-develop paradigm allows one to incrementally develop programs from their specifications using a series of calculations against the remaining proof obligations. This paper presents a derivation method for real-time systems with realistic constraints on their behaviour. We develop a high-level interval-based logic that provides flexibility in an implementation, yet allows algebraic reasoning over multiple granularities and sampling multiple sensors with delay. The semantics of an action system is given in terms of interval predicates and algebraic operators to unify the logics for an action system and its properties, which in turn simplifies the calculations and derivations.
登录
查看更多内容
关于循环的代数推理
影响因子：
0.6
作者：
R. Back;Joakim von Wright
通讯作者：
Joakim von Wright
关于目标导向的实时远程反应程序的推理
影响因子：
1
作者：
Brijesh Dongol;I. Hayes;P. Robinson
通讯作者：
P. Robinson
影响因子：
0.6
作者：
I. Hayes;M. Utting
通讯作者：
M. Utting
一种多道程序设计方法
DOI：
--
发表时间：
2010
期刊：
Monographs in Computer Science
影响因子：
--
作者：
David Gries;Fred B. Schneider
通讯作者：
Fred B. Schneider
时间的细化
影响因子：
1.1
作者：
M. Broy
通讯作者：
M. Broy