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

Informaatioteknologia

Tutkimustuotos: Artikkeli kirjassa/raportissa/konferenssijulkaisussa › Konferenssiartikkeli › Tieteellinen › vertaisarvioitu

2 Sitaatiot (Scopus)

Abstrakti

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.

Alkuperäiskieli	Ei tiedossa
Otsikko	2018 16th ACM/IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE 2018)
Toimittajat	Derler Patricia, Gao Sicun
Kustantaja	IEEE
Sivut	1–10
ISBN (elektroninen)	978-1-5386-6195-6
ISBN (painettu)	978-1-5386-6196-3
DOI - pysyväislinkit	https://doi.org/10.1109/MEMCOD.2018.8557004
Tila	Julkaistu - 2018
OKM-julkaisutyyppi	A4 Artikkeli konferenssijulkaisuussa
Tapahtuma	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) Kesto: 15 lokak. 2018 → 17 lokak. 2018

Konferenssi

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

Keywords

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

Pääsy asiakirjaan

10.1109/MEMCOD.2018.8557004

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

1 Päättynyt

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

Viittausmuodot

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

Tutkimustuotos: Artikkeli kirjassa/raportissa/konferenssijulkaisussa › Konferenssiartikkeli › Tieteellinen › vertaisarvioitu

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

Abstrakti

Konferenssi

Keywords

Pääsy asiakirjaan

Projektit

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

Viittausmuodot