Verification of concurrent design patterns with data - Coordination Models and Languages Access content directly
Conference Papers Year : 2019

Verification of concurrent design patterns with data


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.
Fichier principal
Vignette du fichier
paper_18.pdf (634.61 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-02143782 , version 1 (29-05-2019)





Simon Bliudze, Ludovic Henrio, Eric Madelaine. Verification of concurrent design patterns with data. COORDINATION 2019 - 21st International Conference on Coordination Models and Languages, Jun 2019, Kongens Lyngby, Denmark. pp.161-181, ⟨10.1007/978-3-030-22397-7_10⟩. ⟨hal-02143782⟩
254 View
205 Download



Gmail Facebook X LinkedIn More