skip to main content
10.1145/2429069.2429120acmconferencesArticle/Chapter ViewAbstractPublication PagespoplConference Proceedingsconference-collections
research-article

Hyperstream processing systems: nonstandard modeling of continuous-time signals

Published: 23 January 2013 Publication History

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

Supplementary Material

JPG File (r1d3_talk4.jpg)
MP4 File (r1d3_talk4.mp4)

References

[1]
S. Abramsky and A. Jung. Domain theory. In S. Abramsky, D. M. Gabbai, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 3, pages 1--168. Oxford Univ. Press, 1994.
[2]
R. Alur, C. Courcoubetis, N. Halbwachs, T. A. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. The algorithmic analysis of hybrid systems. Theor. Comp. Sci., 138(1): 3--34, 1995.
[3]
R. Beauxis and S. Mimram. A non-standard semantics for Kahn networks in continuous time. In M. Bezem, editor, CSL, volume 12 of LIPIcs, pages 35--50. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2011. ISBN 978-3-939897-32-3.
[4]
A. Benveniste, T. Bourke, B. Caillaud, and M. Pouzet. Divide and recycle: types and compilation for a hybrid synchronous language. In J. Vitek and B. D. Sutter, editors, LCTES, pages 61--70. ACM, 2011.
[5]
A. Benveniste, T. Bourke, B. Caillaud, and M. Pouzet. Non-standard semantics of hybrid systems modelers. J. Comput. Syst. Sci., 78 (3): 877--910, 2012.
[6]
S. Bliudze and D. Krob. Modelling of complex systems: Systems as dataflow machines. Fundam. Inform., 91 (2): 251--274, 2009.
[7]
O. Bouissou and A. Chapoutot. An operational semantics for Simulink's simulation engine. In R. Wilhelm, H. Falk, and W. Yi, editors, LCTES, pages 129--138. ACM, 2012. ISBN 978--1--4503--1212--7.
[8]
M. L. Bujorianu and J. Lygeros. Theoretical foundations of stochastic hybrid systems. In International Symposium on Mathematical Theory of Networks and Systems (MTNS 2004), 2004.
[9]
P. Caspi, D. Pilaud, N. Halbwachs, and J. Plaice. Lustre: A declarative language for programming synchronous systems. In POPL, pages 214--227. ACM Press, 1987. ISBN 0--89791--215--2.
[10]
A. Chapoutot and M. Martel. Abstract simulation: A static analysis of simulink models. In T. Chen, D. N. Serpanos, and W. Taha, editors, ICESS, pages 83--92. IEEE, 2009.
[11]
A. Gamatié and L. Gonnord. Static analysis of synchronous programs in signal for efficient design of multi-clocked embedded systems. In J. Vitek and B. D. Sutter, editors, LCTES, pages 71--80. ACM, 2011.
[12]
R. Goldblatt. Lectures on the Hyperreals: An Introduction to Nonstandard Analysis. Springer-Verlag, 1998.
[13]
I. Hasuo and K. Suenaga. Exercises in phNonstandard Static Analysis of hybrid systems. In P. Madhusudan and S. A. Seshia, editors, CAV, volume 7358 of Lect. Notes Comp. Sci., pages 462--478. Springer, 2012.
[14]
A. E. Hurd and P. A. Loeb. An Introduction to Nonstandard Real Analysis. Academic Press, 1985.
[15]
G. Kahn. The semantics of simple language for parallel programming. In IFIP Congress, pages 471--475, 1974.
[16]
N. R. Krishnaswami and N. Benton. Ultrametric semantics of reactive programs. In LICS, pages 257--266. IEEE Computer Society, 2011. ISBN 978-0--7695--4412-0.
[17]
E. A. Lee and H. Zheng. Operational semantics of hybrid systems. IncitetDBLP:conf/hybrid/2005, pages 25--53. ISBN 3--540--25108--1.
[18]
Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer, 1995. ISBN 978-0--387--94459--3.
[19]
M. Morari and L. Thiele, editors. Hybrid Systems: Computation and Control, 8th International Workshop, HSCC 2005, Zurich, Switzerland, March 9--11, 2005, Proceedings, volume 3414 of Lecture Notes in Computer Science, 2005. Springer. ISBN 3--540--25108--1.
[20]
H. Nakano. A modality for recursion. In LICS, pages 255--266. IEEE Computer Society, 2000. ISBN 0--7695-0725--5.
[21]
A. Platzer. Logical Analysis of Hybrid Systems--Proving Theorems for Complex Dynamics. Springer, 2010. ISBN 978--3--642--14508--7.
[22]
A. Platzer. Stochastic differential dynamic logic for stochastic hybrid programs. In N. Bjørner and V. Sofronie-Stokkermans, editors, CADE, volume 6803 of Lecture Notes in Computer Science, pages 446--460. Springer, 2011. ISBN 978--3--642--22437--9.
[23]
A. Platzer. The complete proof theory of hybrid systems. In LICS, 2012.
[24]
A. Robinson. Non-standard analysis. Princeton Univ. Press, 1996.
[25]
E. Rodríguez-Carbonell and A. Tiwari. Generating polynomial invariants for hybrid systems. IncitetDBLP:conf/hybrid/2005, pages 590--605. ISBN 3--540--25108--1.
[26]
S. Sankaranarayanan. Automatic invariant generation for hybrid systems using ideal fixed points. In K. H. Johansson and W. Yi, editors, HSCC, pages 221--230. ACM, 2010. ISBN 978--1--60558--955--8.
[27]
S. Sankaranarayanan, H. B. Sipma, and Z. Manna. Constructing invariants for hybrid systems. Formal Meth. in Sys. Design, 32 (1): 25--55, 2008.
[28]
P. Schrammel and B. Jeannet. From hybrid data-flow languages to hybrid automata: a complete translation. In T. Dang and I. M. Mitchell, editors, HSCC, pages 167--176. ACM, 2012. ISBN 978--1--4503--1220--2.
[29]
R. Stephens. A survey of stream processing. Acta Inf., 34 (7): 491--541, 1997.
[30]
K. Suenaga and I. Hasuo. Programming with infinitesimals: A while-language for hybrid system modeling. In L. Aceto, M. Henzinger, and J. Sgall, editors, ICALP (2), volume 6756 of Lect. Notes Comp. Sci., pages 392--403. Springer, 2011. ISBN 978--3--642--22011--1.
[31]
K. Suenaga, H. Sekine, and I. Hasuo. Hyperstream processing systems: Nonstandard modeling of continuous signal processing. Extended version with proofs, 2013.www-mmm.is.s.u-tokyo.ac.jp/ ichiro/papers.html
[32]
T. Terauchi. Dependent types from counterexamples. In M. V. Hermenegildo and J. Palsberg, editors, POPL, pages 119--130. ACM, 2010. ISBN 978--1--60558--479--9.
[33]
S. Tripakis, C. Sofronis, P. Caspi, and A. Curic. Translating discrete-time simulink to Lustre. ACM Trans. Embedded Comput. Syst., 4 (4): 779--818, 2005.
[34]
Z. Wan and P. Hudak. Functional reactive programming from first principles. In M. S. Lam, editor, PLDI, pages 242--252. ACM, 2000. ISBN 1--58113--199--2.
[35]
K. R. Wicks. Nonstandard analysis of ordered sets. Order, 12: 265--293, 1995.

Cited By

View all
  • (2020)Relational Differential Dynamic LogicTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-030-45190-5_11(191-208)Online publication date: 17-Apr-2020
  • (2020)Generalized Property-Directed Reachability for Hybrid SystemsVerification, Model Checking, and Abstract Interpretation10.1007/978-3-030-39322-9_14(293-313)Online publication date: 16-Jan-2020
  • (2019)Nonstandard Static Analysis: Literal Transfer of Deductive Verification Frameworks from Discrete to HybridCyber Physical Systems. Design, Modeling, and Evaluation10.1007/978-3-030-17910-6_1(3-7)Online publication date: 13-Apr-2019
  • Show More Cited By

Index Terms

  1. Hyperstream processing systems: nonstandard modeling of continuous-time signals

        Recommendations

        Comments

        Information & Contributors

        Information

        Published In

        cover image ACM Conferences
        POPL '13: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
        January 2013
        586 pages
        ISBN:9781450318327
        DOI:10.1145/2429069
        • cover image ACM SIGPLAN Notices
          ACM SIGPLAN Notices  Volume 48, Issue 1
          POPL '13
          January 2013
          561 pages
          ISSN:0362-1340
          EISSN:1558-1160
          DOI:10.1145/2480359
          Issue’s Table of Contents
        Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

        Sponsors

        In-Cooperation

        Publisher

        Association for Computing Machinery

        New York, NY, United States

        Publication History

        Published: 23 January 2013

        Permissions

        Request permissions for this article.

        Check for updates

        Author Tags

        1. hybrid system
        2. nonstandard analysis
        3. signal processing
        4. stream processing
        5. type system

        Qualifiers

        • Research-article

        Conference

        POPL '13
        Sponsor:

        Acceptance Rates

        Overall Acceptance Rate 860 of 4,328 submissions, 20%

        Upcoming Conference

        POPL '26

        Contributors

        Other Metrics

        Bibliometrics & Citations

        Bibliometrics

        Article Metrics

        • Downloads (Last 12 months)3
        • Downloads (Last 6 weeks)1
        Reflects downloads up to 19 Feb 2025

        Other Metrics

        Citations

        Cited By

        View all
        • (2020)Relational Differential Dynamic LogicTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-030-45190-5_11(191-208)Online publication date: 17-Apr-2020
        • (2020)Generalized Property-Directed Reachability for Hybrid SystemsVerification, Model Checking, and Abstract Interpretation10.1007/978-3-030-39322-9_14(293-313)Online publication date: 16-Jan-2020
        • (2019)Nonstandard Static Analysis: Literal Transfer of Deductive Verification Frameworks from Discrete to HybridCyber Physical Systems. Design, Modeling, and Evaluation10.1007/978-3-030-17910-6_1(3-7)Online publication date: 13-Apr-2019
        • (2018)Building a Hybrid Systems Modeler on Synchronous Languages PrinciplesProceedings of the IEEE10.1109/JPROC.2018.2858016106:9(1568-1592)Online publication date: Sep-2018
        • (2017)A Synchronous Look at the Simulink Standard LibraryACM Transactions on Embedded Computing Systems10.1145/312651616:5s(1-24)Online publication date: 27-Sep-2017
        • (2017)Reverse formalism 16Synthese10.1007/s11229-017-1322-2Online publication date: 7-Feb-2017
        • (2017)Metamathematics for Systems DesignNew Generation Computing10.1007/s00354-017-0023-135:3(271-305)Online publication date: 15-Jul-2017
        • (2017)A Nonstandard Functional Programming LanguageProgramming Languages and Systems10.1007/978-3-319-71237-6_25(514-533)Online publication date: 19-Nov-2017
        • (2016)Generalized Homogeneous Polynomials for Efficient Template-Based Nonlinear Invariant SynthesisStatic Analysis10.1007/978-3-662-53413-7_14(278-299)Online publication date: 31-Aug-2016
        • (2016)Abstract Interpretation with InfinitesimalsProceedings of the 17th International Conference on Verification, Model Checking, and Abstract Interpretation - Volume 958310.1007/978-3-662-49122-5_11(229-249)Online publication date: 17-Jan-2016
        • Show More Cited By

        View Options

        Login options

        View options

        PDF

        View or Download as a PDF file.

        PDF

        eReader

        View online with eReader.

        eReader

        Figures

        Tables

        Media

        Share

        Share

        Share this Publication link

        Share on social media