Specification and Automated Verification of Dynamic Dataflow Networks

Jonatan Wiik, Pontus Boström

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

    2 Citations (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 Sept 20178 Sept 2017


    ConferenceInternational Conference on Software Engineering and Formal Methods (SEFM)

    Cite this