Title :

Verification of concurrent design patterns with data

Author(s) :

Bliudze, Simon [Auteur]
Self-adaptation for distributed services and large software systems [SPIRALS]
Henrio, Ludovic [Auteur]
Laboratoire de l'Informatique du Parallélisme [LIP]
CASH - Compilation and Analysis, Software and Hardware [CASH]
Madelaine, Eric [Auteur]
Logical Time for Formal Embedded System Design [KAIROS]

Scientific editor(s) :

Hanne Riis Nielson
Emilio Tuosto

Conference title :

COORDINATION 2019 - 21st International Conference on Coordination Models and Languages

City :

Kongens Lyngby

Country :

Danemark

Start date of the conference :

2019-06-17

Book title :

Lecture Notes in Computer Science

Journal title :

Coordination Models and Languages

Publisher :

Springer International Publishing

Publication date :

2019

English keyword(s) :

interaction models
Symbolic verification
composition
safety

HAL domain(s) :

Informatique [cs]/Calcul parallèle, distribué et partagé [cs.DC]
Informatique [cs]
Informatique [cs]/Réseaux et télécommunications [cs.NI]

English abstract : [en]

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 ...
Show more >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.Show less >

Language :

Anglais

Peer reviewed article :

Oui

Audience :

Internationale

Popular science :

Non

Comment :

t Part 4: Coordination Patterns

Collections :

• Centre de Recherche en Informatique, Signal et Automatique de Lille (CRIStAL) - UMR 9189

Source :

Harvested from HAL