Hyperstream Processing Systems: Nonstandard Modeling of Continuous-Time Signals

摘要

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.