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

Résultats de recherche: Le chapitre dans un livre, un rapport, une anthologie ou une collection › Contribution à une conférence › Revue par des pairs

Résumé

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.

langue originale	Anglais
titre	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
rédacteurs en chef	Emilio Tuosto, Emilio Tuosto, Hanne Riis Nielson
Editeur	Springer Verlag
Pages	161-181
Nombre de pages	21
ISBN (imprimé)	9783030223960
Les DOIs	https://doi.org/10.1007/978-3-030-22397-7_10
état	Publié - 1 janv. 2019
Evénement	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, Danemark Durée: 17 juin 2019 → 21 juin 2019

Série de publications

Nom	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	11533 LNCS
ISSN (imprimé)	0302-9743
ISSN (Electronique)	1611-3349

Une conférence

Une conférence	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
Pays/Territoire	Danemark
La ville	Kongens Lyngby
période	17/06/19 → 21/06/19

Accès au document

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

Autres fichiers et liens

Lien vers la publication dans Scopus

Contient cette citation

Bliudze, S., Henrio, L., & Madelaine, E. (2019). Verification of concurrent design patterns with data. Dans 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 (p. 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. Editeur / 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)).

@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. Dans 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, p. 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, Danemark, 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).

Résultats de recherche: Le chapitre dans un livre, un rapport, une anthologie ou une collection › Contribution à une conférence › Revue par des pairs

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

UR - https://www.scopus.com/pages/publications/85067456990

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. Dans Tuosto E, Tuosto E, Riis Nielson H, rédacteurs en chef, 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

Résumé

Série de publications

Une conférence

Accès au document

Autres fichiers et liens

Empreinte digitale

Contient cette citation