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)

    Abstract

    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
    PublisherSpringer
    Pages136–151
    ISBN (Electronic)978-3-319-66197-1
    ISBN (Print)978-3-319-66196-4
    DOIs
    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

    Conference

    ConferenceInternational Conference on Software Engineering and Formal Methods (SEFM)
    Period04/09/1708/09/17

    Cite this