2026-07-21T23:54:35Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:14781 2024-03-06T10:54:37Z ddc:004 open_access

Model Checking of Stream Processing Pipelines Bédard, Alexis Hallé, Sylvain stream processing model checking 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Alexis Bédard and Sylvain Hallé 2021 Is Part Of LIPIcs, Volume 206, 28th International Symposium on Temporal Representation and Reasoning (TIME 2021) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TIME.2021.5 urn:nbn:de:0030-drops-147819 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2021.5 eng https://creativecommons.org/licenses/by/4.0/legalcode