Hyperstream processing systems: nonstandard modeling of continuous-time signals
Hyperstream processing systems: nonstandard modeling of continuous-time signals
复制标题
DOI：
10.1145/2429069.2429120
复制
发表时间：
2013-01
期刊：
影响因子：
--
通讯作者：
Kohei Suenaga;Hiroyoshi Sekine;I. Hasuo
中科院分区：
文献类型：
--
作者：
Kohei Suenaga;Hiroyoshi Sekine;I. Hasuo
我们利用（离散时间）流处理与（连续时间）信号处理之间的明显相似性，并将演绎验证框架从前者转移到后者。我们的发展基于依赖于非标准分析（NSA）的严格语义。具体来说，我们从一个离散的框架开始，该框架由Lustre式的流处理语言，其KAHN风格的固定点语义和程序逻辑（以类型系统的形式）组成，以保证部分正确性。该流框架被转移到一个流向流的流中，这通常是由NSA的逻辑基础结构逐渐较小的抽样（连续时间）信号引起的。在一定的连续性假设下，我们识别具有信号的超流；因此，我们获得的最终结果是信号的演绎验证框架。在其中，人们使用（常规离散的）证明原理（如固定点诱导）验证了信号的属性。
We exploit the apparent similarity between (discrete-time) stream processing and (continuous-time) signal processing and transfer a deductive verification framework from the former to the latter. Our development is based on rigorous semantics that relies on nonstandard analysis (NSA). Specifically, we start with a discrete framework consisting of a Lustre-like stream processing language, its Kahn-style fixed point semantics, and a program logic (in the form of a type system) for partial correctness guarantees. This stream framework is transferred as it is to one for hyperstreams---streams of streams, that typically arise from sampling (continuous-time) signals with progressively smaller intervals---via the logical infrastructure of NSA. Under a certain continuity assumption we identify hyperstreams with signals; our final outcome thus obtained is a deductive verification framework of signals. In it one verifies properties of signals using the (conventionally discrete) proof principles, like fixed point induction.