Where academic tradition
meets the exciting future

Contract-Based Specification and Verification of Dataflow Programs

Jonatan Wiik, Pontus Boström, Contract-Based Specification and Verification of Dataflow Programs. In: Luca Aceto, Anna Ingolfsdottir (Eds.), Proceedings of 27th Nordic Workshop on Programming Theory, NWPT'15, 1–3, Reykjavik University, 2015.

Abstract:

We present an approach to specification and automatic verification of dataflow programs based on assume-guarantee reasoning. The programs consist of networks of actors connected via asynchronous channels that describe the flow of data between actors. The approach is based on annotating actors and networks with contracts stating functional properties which the actor or network should adhere to. The goal of the approach is to ensure functional correctness with respect to the contracts as well as deadlock freedom for dataflow networks.

Files:

Full publication in PDF-format

BibTeX entry:

@INPROCEEDINGS{inpWiBo15a,
  title = {Contract-Based Specification and Verification of Dataflow Programs},
  booktitle = {Proceedings of 27th Nordic Workshop on Programming Theory, NWPT'15},
  author = {Wiik, Jonatan and Boström, Pontus},
  editor = {Aceto, Luca and Ingolfsdottir, Anna},
  publisher = {Reykjavik University},
  pages = {1–3},
  year = {2015},
}

Belongs to TUCS Research Unit(s): Distributed Systems Laboratory (DS Lab)

Edit publication