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

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

2 Sitaatiot (Scopus)

Abstrakti

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.

Alkuperäiskieli	Ei tiedossa
Otsikko	Software Engineering and Formal Methods: 15th International Conference, SEFM 2017, Proceedings
Toimittajat	Alessandro Cimatti, Marjan Sirjani
Kustantaja	Springer
Sivut	136–151
ISBN (elektroninen)	978-3-319-66197-1
ISBN (painettu)	978-3-319-66196-4
DOI - pysyväislinkit	https://doi.org/10.1007/978-3-319-66197-1_9
Tila	Julkaistu - 2017
OKM-julkaisutyyppi	A4 Artikkeli konferenssijulkaisuussa
Tapahtuma	International Conference on Software Engineering and Formal Methods (SEFM) - 15th International Conference on Software Engineering and Formal Methods. SEFM 2017 Kesto: 4 syysk. 2017 → 8 syysk. 2017

Konferenssi

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

Pääsy asiakirjaan

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

1 Päättynyt

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
Projekti: Research Council of Finland/Other Research Councils

Viittausmuodot

@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. julkaisussa A Cimatti & M Sirjani (toim), Software Engineering and Formal Methods: 15th International Conference, SEFM 2017, Proceedings. Springer, Sivut 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. toim. / Alessandro Cimatti; Marjan Sirjani. Springer, 2017. s. 136–151.

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

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

Abstrakti

Konferenssi

Pääsy asiakirjaan

Projektit

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

Viittausmuodot