Specification and Automated Verification of Dynamic Dataflow Networks

Jonatan Wiik; Pontus Boström

doi:10.1007/978-3-319-66197-1_9

Specification and Automated Verification of Dynamic Dataflow Networks

Jonatan Wiik, Pontus Boström

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

2 Citeringar (Scopus)

Sammanfattning

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.

Originalspråk	Odefinierat/okänt
Titel på värdpublikation	Software Engineering and Formal Methods: 15th International Conference, SEFM 2017, Proceedings
Redaktörer	Alessandro Cimatti, Marjan Sirjani
Förlag	Springer
Sidor	136–151
ISBN (elektroniskt)	978-3-319-66197-1
ISBN (tryckt)	978-3-319-66196-4
DOI	https://doi.org/10.1007/978-3-319-66197-1_9
Status	Publicerad - 2017
MoE-publikationstyp	A4 Artikel i en konferenspublikation
Evenemang	International Conference on Software Engineering and Formal Methods (SEFM) - 15th International Conference on Software Engineering and Formal Methods. SEFM 2017 Varaktighet: 4 sep. 2017 → 8 sep. 2017

Konferens

Konferens	International Conference on Software Engineering and Formal Methods (SEFM)
Period	04/09/17 → 08/09/17

Åtkomst av dokument

10.1007/978-3-319-66197-1_9

1 Slutfört

ADVICeS: Adaptive Integrated Formal Design of Safety-Critical Systems (Academy of Finland)
Walden, M., Olszewska, M., Edmunds, A., Ostroumov, S., Petre, L., Boström, P. & Neovius, M.
01/09/13 → 31/08/17
Projekt: Finlands Akademi/Övriga Forskningsråd

Citera det här

@inproceedings{257fe4c980db4fd5a8825421cf934dcf,

title = "Specification and Automated Verification of Dynamic Dataflow Networks",

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.",

author = "Jonatan Wiik and Pontus Bostr{\"o}m",

year = "2017",

doi = "10.1007/978-3-319-66197-1_9",

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

isbn = "978-3-319-66196-4",

pages = "136–151",

editor = "Alessandro Cimatti and Marjan Sirjani",

booktitle = "Software Engineering and Formal Methods: 15th International Conference, SEFM 2017, Proceedings",

publisher = "Springer",

note = "International Conference on Software Engineering and Formal Methods (SEFM) ; Conference date: 04-09-2017 Through 08-09-2017",

}

Wiik, J & Boström, P 2017, Specification and Automated Verification of Dynamic Dataflow Networks. i A Cimatti & M Sirjani (red), Software Engineering and Formal Methods: 15th International Conference, SEFM 2017, Proceedings. Springer, s. 136–151, International Conference on Software Engineering and Formal Methods (SEFM), 04/09/17. https://doi.org/10.1007/978-3-319-66197-1_9

Specification and Automated Verification of Dynamic Dataflow Networks. / Wiik, Jonatan; Boström, Pontus.
Software Engineering and Formal Methods: 15th International Conference, SEFM 2017, Proceedings. red. / Alessandro Cimatti; Marjan Sirjani. Springer, 2017. s. 136–151.

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

TY - GEN

T1 - Specification and Automated Verification of Dynamic Dataflow Networks

AU - Wiik, Jonatan

AU - Boström, Pontus

PY - 2017

Y1 - 2017

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-319-66197-1_9

DO - 10.1007/978-3-319-66197-1_9

M3 - Konferensbidrag

SN - 978-3-319-66196-4

SP - 136

EP - 151

BT - Software Engineering and Formal Methods: 15th International Conference, SEFM 2017, Proceedings

A2 - Cimatti, Alessandro

A2 - Sirjani, Marjan

PB - Springer

T2 - International Conference on Software Engineering and Formal Methods (SEFM)

Y2 - 4 September 2017 through 8 September 2017

ER -

Specification and Automated Verification of Dynamic Dataflow Networks

Sammanfattning

Konferens

Åtkomst av dokument

Projekt

ADVICeS: Adaptive Integrated Formal Design of Safety-Critical Systems (Academy of Finland)

Citera det här