Verification of concurrent design patterns with data

Simon Bliudze; Ludovic Henrio; Eric Madelaine

doi:10.1007/978-3-030-22397-7_10

Verification of concurrent design patterns with data

Simon Bliudze
, Ludovic Henrio
, Eric Madelaine

École Polytechnique

ENS Lyon
Université Côte D’Azur

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

Abstract

We provide a solution for the design of safe concurrent systems by compositional application of verified design patterns—called architectures—to a small set of functional components. To this end, we extend the theory of architectures developed previously for the BIP framework with the elements necessary for handling data: definition and operations on data domains, syntax and semantics of composition operators involving data transfer. We provide a set of conditions under which composition of architectures preserves their characteristic safety properties. To verify that individual architectures do enforce their associated properties, we provide an encoding into open pNets, an intermediate model that supports SMT-based verification. The approach is illustrated by a case study based on a previously developed BIP model of a nanosatellite on-board software.

Original language	English
Title of host publication	Coordination Models and Languages - 21st IFIP WG 6.1 International Conference, COORDINATION 2019, Held as Part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019, Proceedings
Editors	Emilio Tuosto, Emilio Tuosto, Hanne Riis Nielson
Publisher	Springer Verlag
Pages	161-181
Number of pages	21
ISBN (Print)	9783030223960
DOIs	https://doi.org/10.1007/978-3-030-22397-7_10
Publication status	Published - 1 Jan 2019
Event	21st IFIP WG 6.1 International Conference on Coordination Models and Languages, COORDINATION 2019 held as part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019 - Kongens Lyngby, Denmark Duration: 17 Jun 2019 → 21 Jun 2019

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	11533 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	21st IFIP WG 6.1 International Conference on Coordination Models and Languages, COORDINATION 2019 held as part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019
Country/Territory	Denmark
City	Kongens Lyngby
Period	17/06/19 → 21/06/19

Keywords

Composition
Interaction models
Safety
Symbolic verification

Access to Document

10.1007/978-3-030-22397-7_10

Cite this

Bliudze, S., Henrio, L., & Madelaine, E. (2019). Verification of concurrent design patterns with data. In E. Tuosto, E. Tuosto, & H. Riis Nielson (Eds.), Coordination Models and Languages - 21st IFIP WG 6.1 International Conference, COORDINATION 2019, Held as Part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019, Proceedings (pp. 161-181). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11533 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-030-22397-7_10

Bliudze, Simon ; Henrio, Ludovic ; Madelaine, Eric. / Verification of concurrent design patterns with data. Coordination Models and Languages - 21st IFIP WG 6.1 International Conference, COORDINATION 2019, Held as Part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019, Proceedings. editor / Emilio Tuosto ; Emilio Tuosto ; Hanne Riis Nielson. Springer Verlag, 2019. pp. 161-181 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{97e87dd822fe40cd925d110817551248,

title = "Verification of concurrent design patterns with data",

abstract = "We provide a solution for the design of safe concurrent systems by compositional application of verified design patterns—called architectures—to a small set of functional components. To this end, we extend the theory of architectures developed previously for the BIP framework with the elements necessary for handling data: definition and operations on data domains, syntax and semantics of composition operators involving data transfer. We provide a set of conditions under which composition of architectures preserves their characteristic safety properties. To verify that individual architectures do enforce their associated properties, we provide an encoding into open pNets, an intermediate model that supports SMT-based verification. The approach is illustrated by a case study based on a previously developed BIP model of a nanosatellite on-board software.",

keywords = "Composition, Interaction models, Safety, Symbolic verification",

author = "Simon Bliudze and Ludovic Henrio and Eric Madelaine",

note = "Publisher Copyright: {\textcopyright} IFIP International Federation for Information Processing 2019.; 21st IFIP WG 6.1 International Conference on Coordination Models and Languages, COORDINATION 2019 held as part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019 ; Conference date: 17-06-2019 Through 21-06-2019",

year = "2019",

month = jan,

day = "1",

doi = "10.1007/978-3-030-22397-7\_10",

language = "English",

isbn = "9783030223960",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "161--181",

editor = "Emilio Tuosto and Emilio Tuosto and \{Riis Nielson\}, Hanne",

booktitle = "Coordination Models and Languages - 21st IFIP WG 6.1 International Conference, COORDINATION 2019, Held as Part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019, Proceedings",

}

Bliudze, S, Henrio, L & Madelaine, E 2019, Verification of concurrent design patterns with data. in E Tuosto, E Tuosto & H Riis Nielson (eds), Coordination Models and Languages - 21st IFIP WG 6.1 International Conference, COORDINATION 2019, Held as Part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11533 LNCS, Springer Verlag, pp. 161-181, 21st IFIP WG 6.1 International Conference on Coordination Models and Languages, COORDINATION 2019 held as part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019, Kongens Lyngby, Denmark, 17/06/19. https://doi.org/10.1007/978-3-030-22397-7_10

Verification of concurrent design patterns with data. / Bliudze, Simon; Henrio, Ludovic; Madelaine, Eric.
Coordination Models and Languages - 21st IFIP WG 6.1 International Conference, COORDINATION 2019, Held as Part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019, Proceedings. ed. / Emilio Tuosto; Emilio Tuosto; Hanne Riis Nielson. Springer Verlag, 2019. p. 161-181 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11533 LNCS).

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

TY - GEN

T1 - Verification of concurrent design patterns with data

AU - Bliudze, Simon

AU - Henrio, Ludovic

AU - Madelaine, Eric

N1 - Publisher Copyright: © IFIP International Federation for Information Processing 2019.

PY - 2019/1/1

Y1 - 2019/1/1

N2 - We provide a solution for the design of safe concurrent systems by compositional application of verified design patterns—called architectures—to a small set of functional components. To this end, we extend the theory of architectures developed previously for the BIP framework with the elements necessary for handling data: definition and operations on data domains, syntax and semantics of composition operators involving data transfer. We provide a set of conditions under which composition of architectures preserves their characteristic safety properties. To verify that individual architectures do enforce their associated properties, we provide an encoding into open pNets, an intermediate model that supports SMT-based verification. The approach is illustrated by a case study based on a previously developed BIP model of a nanosatellite on-board software.

AB - We provide a solution for the design of safe concurrent systems by compositional application of verified design patterns—called architectures—to a small set of functional components. To this end, we extend the theory of architectures developed previously for the BIP framework with the elements necessary for handling data: definition and operations on data domains, syntax and semantics of composition operators involving data transfer. We provide a set of conditions under which composition of architectures preserves their characteristic safety properties. To verify that individual architectures do enforce their associated properties, we provide an encoding into open pNets, an intermediate model that supports SMT-based verification. The approach is illustrated by a case study based on a previously developed BIP model of a nanosatellite on-board software.

KW - Composition

KW - Interaction models

KW - Safety

KW - Symbolic verification

U2 - 10.1007/978-3-030-22397-7_10

DO - 10.1007/978-3-030-22397-7_10

M3 - Conference contribution

AN - SCOPUS:85067456990

SN - 9783030223960

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 161

EP - 181

BT - Coordination Models and Languages - 21st IFIP WG 6.1 International Conference, COORDINATION 2019, Held as Part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019, Proceedings

A2 - Tuosto, Emilio

A2 - Riis Nielson, Hanne

PB - Springer Verlag

T2 - 21st IFIP WG 6.1 International Conference on Coordination Models and Languages, COORDINATION 2019 held as part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019

Y2 - 17 June 2019 through 21 June 2019

ER -

Bliudze S, Henrio L, Madelaine E. Verification of concurrent design patterns with data. In Tuosto E, Tuosto E, Riis Nielson H, editors, Coordination Models and Languages - 21st IFIP WG 6.1 International Conference, COORDINATION 2019, Held as Part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019, Proceedings. Springer Verlag. 2019. p. 161-181. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-22397-7_10

Verification of concurrent design patterns with data

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this