Hyperstream Processing Systems Nonstandard Modeling of Continuous-Time Signals
Hyperstream Processing Systems Nonstandard Modeling of Continuous-Time Signals
复制标题
DOI：
10.1145/2480359.2429120
复制
发表时间：
2013-01-01
影响因子：
--
通讯作者：
Hasuo, Ichiro
中科院分区：
文献类型：
--
作者：
Suenaga, Kohei;Sekine, Hiroyoshi;Hasuo, Ichiro
我们利用(离散时间)流处理和(连续时间)信号处理之间的明显相似性，并将演绎验证框架从前者转移到后者。我们的开发基于严格的语义，依赖于非标准分析(NSA)。具体地说，我们从一个离散框架开始，该框架由一种类似Lustre的流处理语言、其Kahn风格的定点语义和用于部分正确性保证的程序逻辑(以类型系统的形式)组成。通过国家安全局的逻辑基础设施，这种流框架原封不动地转移到用于超级流的框架--流的流，通常产生于以逐渐变小的间隔采样(连续时间)信号。在一定的连续性假设下，我们将超流与信号进行识别；由此得到的最终结果是信号的演绎验证框架。在它中，人们使用(传统上是离散的)证明原理，如不动点归纳来验证信号的性质。
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.