A Contract-Based Approach to Scheduling and Verification of Dynamic Dataflow Networks

Jonatan Wiik; Johan Ersfolk; Marina Walden

doi:10.1109/MEMCOD.2018.8557004

A Contract-Based Approach to Scheduling and Verification of Dynamic Dataflow Networks

Jonatan Wiik, Johan Ersfolk, Marina Walden

Information Technology

Research output: Chapter in Book/Conference proceeding › Conference contribution › Scientific › peer-review

2 Citations (Scopus)

Abstract

Restricted dataflow models of computation have gained widespread adoption in the safety-critical and real-time domains. As more complex functionality is being incorporated in embedded systems, there is a need for more expressive languages while maintaining high analysability. We present a contract-based approach to specification, scheduling and verification of dynamic dataflow networks. The approach is based on finding static schedules based on contracts and utilising this information in the verification process to reduce the number of invariant annotations needed. Moreover, we show that contracts can be used to make compile-time scheduling decisions, hence, improving runtime performance.

Original language	Undefined/Unknown
Title of host publication	2018 16th ACM/IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE 2018)
Editors	Derler Patricia, Gao Sicun
Publisher	IEEE
Pages	1–10
ISBN (Electronic)	978-1-5386-6195-6
ISBN (Print)	978-1-5386-6196-3
DOIs	https://doi.org/10.1109/MEMCOD.2018.8557004
Publication status	Published - 2018
MoE publication type	A4 Article in a conference publication
Event	16th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE2018) - 16th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE2018) Duration: 15 Oct 2018 → 17 Oct 2018

Conference

Conference	16th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE2018)
Period	15/10/18 → 17/10/18

Keywords

Dataflow programming
Design-by-Contract
Formal verification
Quasi-static scheduling

Access to Document

10.1109/MEMCOD.2018.8557004

https://ieeexplore.ieee.org/document/8557004

1 Finished

MERGE: Merging digital hydraulic systems and supercomputing (Academy of Finland)
Walden, M., Westerholm, J., Boström, P., Ersfolk, J. & Wiik, J.
01/01/15 → 31/12/16
Project: Research Council of Finland/Other Research Councils

Cite this

@inproceedings{36ee4173e0084ae289b5eef70118c527,

title = "A Contract-Based Approach to Scheduling and Verification of Dynamic Dataflow Networks",

abstract = "Restricted dataflow models of computation have gained widespread adoption in the safety-critical and real-time domains. As more complex functionality is being incorporated in embedded systems, there is a need for more expressive languages while maintaining high analysability. We present a contract-based approach to specification, scheduling and verification of dynamic dataflow networks. The approach is based on finding static schedules based on contracts and utilising this information in the verification process to reduce the number of invariant annotations needed. Moreover, we show that contracts can be used to make compile-time scheduling decisions, hence, improving runtime performance.",

keywords = "Dataflow programming, Design-by-Contract, Formal verification, Quasi-static scheduling, Dataflow programming, Design-by-Contract, Formal verification, Quasi-static scheduling, Dataflow programming, Design-by-Contract, Formal verification, Quasi-static scheduling",

author = "Jonatan Wiik and Johan Ersfolk and Marina Walden",

year = "2018",

doi = "10.1109/MEMCOD.2018.8557004",

language = "Odefinierat/ok{\"a}nt",

isbn = "978-1-5386-6196-3",

pages = "1–10",

editor = "Derler Patricia and Gao Sicun",

booktitle = "2018 16th ACM/IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE 2018)",

publisher = "IEEE",

note = "16th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE2018) ; Conference date: 15-10-2018 Through 17-10-2018",

}

Wiik, J, Ersfolk, J & Walden, M 2018, A Contract-Based Approach to Scheduling and Verification of Dynamic Dataflow Networks. in D Patricia & G Sicun (eds), 2018 16th ACM/IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE 2018). IEEE, pp. 1–10, 16th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE2018), 15/10/18. https://doi.org/10.1109/MEMCOD.2018.8557004

A Contract-Based Approach to Scheduling and Verification of Dynamic Dataflow Networks. / Wiik, Jonatan; Ersfolk, Johan; Walden, Marina.
2018 16th ACM/IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE 2018). ed. / Derler Patricia; Gao Sicun. IEEE, 2018. p. 1–10.

Research output: Chapter in Book/Conference proceeding › Conference contribution › Scientific › peer-review

TY - GEN

T1 - A Contract-Based Approach to Scheduling and Verification of Dynamic Dataflow Networks

AU - Wiik, Jonatan

AU - Ersfolk, Johan

AU - Walden, Marina

PY - 2018

Y1 - 2018

N2 - Restricted dataflow models of computation have gained widespread adoption in the safety-critical and real-time domains. As more complex functionality is being incorporated in embedded systems, there is a need for more expressive languages while maintaining high analysability. We present a contract-based approach to specification, scheduling and verification of dynamic dataflow networks. The approach is based on finding static schedules based on contracts and utilising this information in the verification process to reduce the number of invariant annotations needed. Moreover, we show that contracts can be used to make compile-time scheduling decisions, hence, improving runtime performance.

AB - Restricted dataflow models of computation have gained widespread adoption in the safety-critical and real-time domains. As more complex functionality is being incorporated in embedded systems, there is a need for more expressive languages while maintaining high analysability. We present a contract-based approach to specification, scheduling and verification of dynamic dataflow networks. The approach is based on finding static schedules based on contracts and utilising this information in the verification process to reduce the number of invariant annotations needed. Moreover, we show that contracts can be used to make compile-time scheduling decisions, hence, improving runtime performance.

KW - Dataflow programming

KW - Design-by-Contract

KW - Formal verification

KW - Quasi-static scheduling

KW - Dataflow programming

KW - Design-by-Contract

KW - Formal verification

KW - Quasi-static scheduling

KW - Dataflow programming

KW - Design-by-Contract

KW - Formal verification

KW - Quasi-static scheduling

U2 - 10.1109/MEMCOD.2018.8557004

DO - 10.1109/MEMCOD.2018.8557004

M3 - Konferensbidrag

SN - 978-1-5386-6196-3

SP - 1

EP - 10

BT - 2018 16th ACM/IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE 2018)

A2 - Patricia, Derler

A2 - Sicun, Gao

PB - IEEE

T2 - 16th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE2018)

Y2 - 15 October 2018 through 17 October 2018

ER -

A Contract-Based Approach to Scheduling and Verification of Dynamic Dataflow Networks

Abstract

Conference

Keywords

Access to Document

Projects

MERGE: Merging digital hydraulic systems and supercomputing (Academy of Finland)

Cite this