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

Informationsteknologi

Forskningsoutput: Kapitel i bok/konferenshandling › Konferensbidrag › Vetenskaplig › Peer review

2 Citeringar (Scopus)

Sammanfattning

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.

Originalspråk	Odefinierat/okänt
Titel på värdpublikation	2018 16th ACM/IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE 2018)
Redaktörer	Derler Patricia, Gao Sicun
Förlag	IEEE
Sidor	1–10
ISBN (elektroniskt)	978-1-5386-6195-6
ISBN (tryckt)	978-1-5386-6196-3
DOI	https://doi.org/10.1109/MEMCOD.2018.8557004
Status	Publicerad - 2018
MoE-publikationstyp	A4 Artikel i en konferenspublikation
Evenemang	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) Varaktighet: 15 okt. 2018 → 17 okt. 2018

Konferens

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

Nyckelord

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

Åtkomst av dokument

10.1109/MEMCOD.2018.8557004

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

1 Slutfört

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
Projekt: Finlands Akademi/Övriga Forskningsråd

Citera det här

@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. i D Patricia & G Sicun (red), 2018 16th ACM/IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE 2018). IEEE, s. 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). red. / Derler Patricia; Gao Sicun. IEEE, 2018. s. 1–10.

Forskningsoutput: Kapitel i bok/konferenshandling › Konferensbidrag › Vetenskaplig › 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

Sammanfattning

Konferens

Nyckelord

Åtkomst av dokument

Projekt

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

Citera det här