Document Open Access Logo

Model Checking of Stream Processing Pipelines

Authors Alexis Bédard, Sylvain Hallé

PDF
Thumbnail PDF

File

LIPIcs.TIME.2021.5.pdf
  • Filesize: 1.03 MB
  • 17 pages

Document Identifiers

Author Details

Alexis Bédard
  • Laboratoire d'informatique formelle, Université du Québec à Chicoutimi, Saguenay, Canada
Sylvain Hallé
  • Laboratoire d'informatique formelle, Université du Québec à Chicoutimi, Saguenay, Canada

Funding

Canada Research Chair on Software Specification, Testing and Verification

Acknowledgements

The open access publication of this article was supported by the Alpen-Adria-Universität Klagenfurt, Austria.

Cite As Get BibTex

Alexis Bédard and Sylvain Hallé. Model Checking of Stream Processing Pipelines. In 28th International Symposium on Temporal Representation and Reasoning (TIME 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 206, pp. 5:1-5:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.TIME.2021.5

Abstract

Event stream processing (ESP) is the application of a computation to a set of input sequences of arbitrary data objects, called "events", in order to produce other sequences of data objects. In recent years, a large number of ESP systems have been developed; however, none of them is easily amenable to a formal verification of properties on their execution. In this paper, we show how stream processing pipelines built with an existing ESP library called BeepBeep 3 can be exported as a Kripke structure for the NuXmv model checker. This makes it possible to formally verify properties on these pipelines, and opens the way to the use of such pipelines directly within a model checker as an extension of its specification language.

Subject Classification

ACM Subject Classification
  • Theory of computation → Streaming models
Keywords
  • stream processing
  • model checking

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Apache Flink. URL: https://flink.apache.org, Accessed April 26th, 2021.
  2. Esper. URL: http://espertech.com.
  3. StreamBase SQL. URL: http://streambase.com.
  4. VoltDB. URL: http://voltdb.com.
  5. Daniel J. Abadi, Yanif Ahmad, Magdalena Balazinska, Ugur Çetintemel, Mitch Cherniack, Jeong-Hyon Hwang, Wolfgang Lindner, Anurag Maskey, Alex Rasin, Esther Ryvkina, Nesime Tatbul, Ying Xing, and Stanley B. Zdonik. The design of the Borealis stream processing engine. In CIDR, pages 277-289, 2005. URL: http://www.cidrdb.org/cidr2005/papers/P23.pdf.
  6. Parosh Aziz Abdulla and Bengt Jonsson. Verifying programs with unreliable channels. Inf. Comput., 127(2):91-101, 1996. URL: https://doi.org/10.1006/inco.1996.0053.
  7. A. Arasu, B. Babcock, S. Babu, J. Cieslewicz, M. Datar, K. Ito, R Motwani, U. Srivastava, and J. Widom. Stream: The stanford data stream management system. Technical Report 2004-20, Stanford InfoLab, 2004. URL: http://ilpubs.stanford.edu:8090/641/.
  8. Ezio Bartocci, Yliès Falcone, Adrian Francalanza, and Giles Reger. Introduction to runtime verification. In Ezio Bartocci and Yliès Falcone, editors, Lectures on Runtime Verification - Introductory and Advanced Topics, volume 10457 of Lecture Notes in Computer Science, pages 1-33. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-75632-5_1.
  9. Edmon Begoli, Tyler Akidau, Fabian Hueske, Julian Hyde, Kathryn Knight, and Kenneth Knowles. One SQL to rule them all - an efficient and syntactically idiomatic approach to management of streams and tables. In Peter A. Boncz, Stefan Manegold, Anastasia Ailamaki, Amol Deshpande, and Tim Kraska, editors, Proceedings of the 2019 International Conference on Management of Data, SIGMOD Conference 2019, Amsterdam, The Netherlands, June 30 - July 5, 2019, pages 1757-1772. ACM, 2019. URL: https://doi.org/10.1145/3299869.3314040.
  10. Quentin Betti, Raphaël Khoury, Sylvain Hallé, and Benoît Montreuil. Improving hyperconnected logistics with blockchains and smart contracts. IT Prof., 21(4):25-32, 2019. URL: https://doi.org/10.1109/MITP.2019.2912135.
  11. Mohamed Recem Boussaha, Raphaël Khoury, and Sylvain Hallé. Monitoring of security properties using BeepBeep. In Abdessamad Imine, José M. Fernandez, Jean-Yves Marion, Luigi Logrippo, and Joaquín García-Alfaro, editors, FPS, volume 10723 of Lecture Notes in Computer Science, pages 160-169. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-75650-9_11.
  12. Lars Brenna, Johannes Gehrke, Mingsheng Hong, and Dag Johansen. Distributed event stream processing with non-deterministic finite automata. In Aniruddha S. Gokhale and Douglas C. Schmidt, editors, DEBS. ACM, 2009. URL: https://doi.org/10.1145/1619258.1619263.
  13. Sirish Chandrasekaran, Owen Cooper, Amol Deshpande, Michael J. Franklin, Joseph M. Hellerstein, Wei Hong, Sailesh Krishnamurthy, Samuel Madden, Vijayshankar Raman, Frederick Reiss, and Mehul A. Shah. TelegraphCQ: Continuous dataflow processing for an uncertain world. In CIDR, 2003. URL: http://www-db.cs.wisc.edu/cidr/cidr2003/program/p24.pdf.
  14. Søren Christensen and Laure Petrucci. Modular analysis of petri nets. Comput. J., 43(3):224-242, 2000. URL: https://doi.org/10.1093/comjnl/43.3.224.
  15. Alessandro Cimatti, Edmund M. Clarke, Fausto Giunchiglia, and Marco Roveri. NuSMV: A new symbolic model checker. Int. J. Softw. Tools Technol. Transf., 2(4):410-425, 2000. URL: https://doi.org/10.1007/s100090050046.
  16. Ben D'Angelo, Sriram Sankaranarayanan, César Sánchez, Will Robinson, Bernd Finkbeiner, Henny B. Sipma, Sandeep Mehrotra, and Zohar Manna. LOLA: runtime monitoring of synchronous systems. In 12th International Symposium on Temporal Representation and Reasoning (TIME 2005), 23-25 June 2005, Burlington, Vermont, USA, pages 166-174. IEEE Computer Society, 2005. URL: https://doi.org/10.1109/TIME.2005.26.
  17. Javier Esparza and Keijo Heljanko. A new unfolding approach to LTL model checking. In Ugo Montanari, José D. P. Rolim, and Emo Welzl, editors, ICALP, volume 1853 of Lecture Notes in Computer Science, pages 475-486. Springer, 2000. URL: https://doi.org/10.1007/3-540-45022-X_40.
  18. Javier Esparza and Keijo Heljanko. Implementing LTL model checking with net unfoldings. In Matthew B. Dwyer, editor, SPIN, volume 2057 of Lecture Notes in Computer Science, pages 37-56. Springer, 2001. URL: https://doi.org/10.1007/3-540-45139-0_4.
  19. Erich Gamma, Richard Helm, Ralph Johnson, and John Vlissides. Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, 1994. Google Scholar
  20. Sylvain Hallé. When RV meets CEP. In Yliès Falcone and César Sánchez, editors, RV, volume 10012 of Lecture Notes in Computer Science, pages 68-91. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-46982-9_6.
  21. Sylvain Hallé, Sébastien Gaboury, and Bruno Bouchard. Activity recognition through complex event processing: First findings. In Bruno Bouchard, Sylvain Giroux, Abdenour Bouzouane, and Sébastien Gaboury, editors, Artificial Intelligence Applied to Assistive Technologies and Smart Environments, Papers from the 2016 AAAI Workshop, Phoenix, Arizona, USA, February 12, 2016, volume WS-16-01 of AAAI Workshops. AAAI Press, 2016. URL: http://www.aaai.org/ocs/index.php/WS/AAAIW16/paper/view/12561.
  22. Sylvain Hallé and Raphaël Khoury. Writing domain-specific languages for BeepBeep. In Christian Colombo and Martin Leucker, editors, RV, volume 11237 of Lecture Notes in Computer Science, pages 447-457. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-03769-7_27.
  23. Sylvain Hallé, Raphaël Khoury, and Mewena Awesso. Streamlining the inclusion of computer experiments in a research paper. Computer, 51(11):78-89, 2018. URL: https://doi.org/10.1109/MC.2018.2876075.
  24. Sylvain Hallé. Event Stream Processing With BeepBeep 3: Log Crunching and Analysis Made Easy. Presses de l'Université du Québec, 2018. Google Scholar
  25. Raphaël Khoury, Sylvain Hallé, and Omar Waldmann. Execution trace analysis using LTL-FO+. In Tiziana Margaria and Bernhard Steffen, editors, ISoLA, volume 9953 of Lecture Notes in Computer Science, pages 356-362, 2016. URL: https://doi.org/10.1007/978-3-319-47169-3_26.
  26. Ramkumar Krishnan, Jonathan Goldstein, and Alex Raizman. A hitchhiker’s guide to StreamInsight queries, version 2.1, 2012. URL: http://support.sas.com/documentation/onlinedoc/dfdmstudio/2.4/dfU_ELRG.pdf.
  27. Timo Latvala and Marko Mäkelä. LTL model checking for modular petri nets. In Jordi Cortadella and Wolfgang Reisig, editors, ICATPN, volume 3099 of Lecture Notes in Computer Science, pages 298-311. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-27793-4_17.
  28. David C. Luckham. The power of events - An introduction to complex event processing in distributed enterprise systems. ACM, 2005. Google Scholar
  29. Nancy A. Lynch and Mark R. Tuttle. Hierarchical correctness proofs for distributed algorithms. In Fred B. Schneider, editor, PODC, pages 137-151. ACM, 1987. URL: https://doi.org/10.1145/41840.41852.
  30. Agnes Madalinski and Victor Khomenko. Predictability verification with parallel ltl-x model checking based on petri net unfoldings. IFAC Proceedings Volumes, 45(20):1232-1237, 2012. Google Scholar
  31. Avinash Malik and David Gregg. Orchestrating stream graphs using model checking. ACM Trans. Archit. Code Optim., 10(3):19:1-19:25, 2013. URL: https://doi.org/10.1145/2512435.
  32. Anca Muscholl. Analysis of communicating automata. In Adrian-Horia Dediu, Henning Fernau, and Carlos Martín-Vide, editors, LATA, volume 6031 of Lecture Notes in Computer Science, pages 50-57. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-13089-2_4.
  33. Srinath Perera, Sriskandarajah Suhothayan, Mohanadarshan Vivekanandalingam, Paul Fremantle, and Sanjiva Weerawarana. Solving the grand challenge using an opensource CEP engine. In Umesh Bellur and Ravi Kothari, editors, DEBS, pages 288-293. ACM, 2014. URL: https://doi.org/10.1145/2611286.2611331.
  34. Stefanie Rinderle-Ma and Sonja Kabicher-Fuchs. An indexing technique for compliance checking and maintenance in large process and rule repositories. Enterp. Model. Inf. Syst. Archit. Int. J. Concept. Model., 11:2:1-2:24, 2016. URL: https://doi.org/10.18417/emisa.11.2.
  35. Abhik Roychoudhury and P. S. Thiagarajan. Communicating transaction processes: An MSC-based model of computation for reactive embedded systems. In Jörg Desel, Wolfgang Reisig, and Grzegorz Rozenberg, editors, Lectures on Concurrency and Petri Nets, Advances in Petri Nets, volume 3098 of Lecture Notes in Computer Science, pages 789-818. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-27755-2_22.
  36. Simon Varvaressos, Kim Lavoie, Sébastien Gaboury, and Sylvain Hallé. Automated bug finding in video games: A case study for runtime monitoring. Computers in Entertainment, 15(1):1:1-1:28, 2017. URL: https://doi.org/10.1145/2700529.
  37. Eugene Wu, Yanlei Diao, and Shariq Rizvi. High-performance complex event processing over streams. In Surajit Chaudhuri, Vagelis Hristidis, and Neoklis Polyzotis, editors, SIGMOD Conference, pages 407-418. ACM, 2006. URL: https://doi.org/10.1145/1142473.1142520.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact