%0 Conference Proceedings
%T Verification of concurrent design patterns with data
%+ Self-adaptation for distributed services and large software systems (SPIRALS)
%+ CASH - Compilation and Analysis, Software and Hardware (CASH)
%+ Laboratoire de l'Informatique du Parallélisme (LIP)
%+ Logical Time for Formal Embedded System Design (KAIROS)
%A Bliudze, Simon
%A Henrio, Ludovic
%A Madelaine, Eric
%Z t Part 4: Coordination Patterns
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B COORDINATION 2019 - 21st International Conference on Coordination Models and Languages
%C Kongens Lyngby, Denmark
%Y Hanne Riis Nielson
%Y Emilio Tuosto
%I Springer International Publishing
%3 Coordination Models and Languages
%V LNCS-11533
%P 161-181
%8 2019-06-17
%D 2019
%R 10.1007/978-3-030-22397-7_10
%K interaction models
%K Symbolic verification
%K composition
%K safety
%Z Computer Science [cs]/Distributed, Parallel, and Cluster Computing [cs.DC]
%Z Computer Science [cs]
%Z Computer Science [cs]/Networking and Internet Architecture [cs.NI]Conference papers
%X We provide a solution for the design of safe concurrent systems by compositional application of verified design patterns-called ar-chitectures-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.
%G English
%Z TC 6
%Z WG 6.1
%2 https://hal.science/hal-02143782/document
%2 https://hal.science/hal-02143782/file/paper_18.pdf
%L hal-02143782
%U https://hal.science/hal-02143782
%~ ENS-LYON
%~ UNICE
%~ CNRS
%~ INRIA
%~ UNIV-LYON1
%~ INRIA-SOPHIA
%~ INRIA-RHA
%~ INRIA-LILLE
%~ I3S
%~ INRIASO
%~ INRIA_TEST
%~ LORIA2
%~ TESTALAIN1
%~ IFIP-LNCS
%~ IFIP
%~ CRISTAL
%~ INRIA2
%~ IFIP-TC
%~ IFIP-WG
%~ CRISTAL-SPIRALS
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ IFIP-COORDINATION
%~ UNIV-COTEDAZUR
%~ INRIA-RENGRE
%~ UNIV-LILLE
%~ IFIP-LNCS-11533
%~ UDL
%~ UNIV-LYON
%~ TEST-HALCNRS