Skip to main content

Hyperstream processing systems: nonstandard modeling of continuous-time signals

Kohei Suenaga, Hiroyoshi Sekine, Ichiro Hasuo

DOI 10.1145/2429069.2429120 dblp BibTeX

Abstract

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).

Related papers

SIGNAL as a Model for Real-Time and Hybrid Systems ESOP 1992
Automated regression testing of BPMN 2.0 processes: a capture and replay framework for continuous delivery GPCE 2016
Bounded model checking of signal temporal logic properties using syntactic separation POPL 2019
Abstract Interpretation with Infinitesimals - Towards Scalability in Nonstandard Static Analysis VMCAI 2016
Using Four-Valued Signal Temporal Logic for Incremental Verification of Hybrid Systems CAV 2024
Safe functional reactive programming through dependent types ICFP 2009
Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants CAV 2017
First-class nonstandard interpretations by opening closures POPL 2007