Titre :

Verification of concurrent design patterns with data

Auteur(s) :

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

Éditeur(s) ou directeur(s) scientifique(s) :

Hanne Riis Nielson
Emilio Tuosto

Titre de la manifestation scientifique :

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

Ville :

Kongens Lyngby

Pays :

Danemark

Date de début de la manifestation scientifique :

2019-06-17

Titre de l’ouvrage :

Lecture Notes in Computer Science

Titre de la revue :

Coordination Models and Languages

Éditeur :

Springer International Publishing

Date de publication :

2019

Mot(s)-clé(s) en anglais :

interaction models
Symbolic verification
composition
safety

Discipline(s) HAL :

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

Résumé en anglais : [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 ...
Lire la suite >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.Lire moins >

Langue :

Anglais

Comité de lecture :

Oui

Audience :

Internationale

Vulgarisation :

Non

Commentaire :

t Part 4: Coordination Patterns

Collections :

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

Source :

Harvested from HAL