Verification of concurrent design patterns with data

Description

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.

Abstract

t Part 4: Coordination Patterns

Abstract

International audience

Additional details