Specification and Automated Verification of Dynamic Dataflow Networks

Jonatan Wiik, Pontus Boström

Research output: Chapter in Book/Conference proceedingConference contributionScientificpeer-review

1 Citation (Scopus)


Dataflow programming has received much recent attention within the signal processing domain as an efficient paradigm for exploiting parallelism. In dataflow programming, systems are modelled as a static network of actors connected through asynchronous order-preserving channels. In this paper we present an approach to contract-based specification and automated verification of dynamic dataflow networks. The verification technique is based on encoding the dataflow networks and contracts in the guarded command language Boogie.

Original languageUndefined/Unknown
Title of host publicationSoftware Engineering and Formal Methods: 15th International Conference, SEFM 2017, Proceedings
EditorsAlessandro Cimatti, Marjan Sirjani
ISBN (Electronic)978-3-319-66197-1
ISBN (Print)978-3-319-66196-4
Publication statusPublished - 2017
MoE publication typeA4 Article in a conference publication
EventInternational Conference on Software Engineering and Formal Methods (SEFM) - 15th International Conference on Software Engineering and Formal Methods. SEFM 2017
Duration: 4 Sep 20178 Sep 2017


ConferenceInternational Conference on Software Engineering and Formal Methods (SEFM)

Cite this