Expressiveness of component-based frameworks: a study of the expressiveness of BIP
- PDF / 1,156,480 Bytes
- 40 Pages / 439.37 x 666.142 pts Page_size
- 91 Downloads / 183 Views
Expressiveness of component-based frameworks: a study of the expressiveness of BIP Eduard Baranov1
· Simon Bliudze2
Received: 8 April 2018 / Accepted: 6 June 2019 © Springer-Verlag GmbH Germany, part of Springer Nature 2019
Abstract We extend our previous algebraic formalisation of the notion of component-based framework in order to formally define two forms—strong and weak—of the notion of full expressiveness and study their properties. Our earlier result shows that the BIP (Behaviour–Interaction– Priority) framework does not possess the strong full expressiveness with respect to the subclass of GSOS rules used for the definition of its semantics. In this paper, we refine this comparison detailing the expressiveness of classical BIP, Offer BIP and a number of variations obtained either by relaxing the constraints in the definition of priority models or by introducing positive premises into the rule formats used to define the operational semantics of composition operators. The obtained results are organised into an expressiveness hierarchy.
1 Introduction In our previous work [3], we have formalised some of the properties that are desirable for component-based design frameworks, namely: incrementality, flattening, compositionality and modularity [24,34]. The formalisation is based on a very simple, abstract algebraic definition of the notion of component-based framework. We have also discussed the full expressiveness property, although without providing a formal definition for it. Intuitively, strong (resp. weak) full expressiveness of one framework w.r.t. another requires that each operator of the first be expressible as an operator (resp. composition of operators) in the second. In this paper, we provide a formal definition of the notion of full expressiveness. We then apply it to study the expressiveness of the BIP (Behaviour–Interaction–Priority) framework [6,7] and their variations.
B
Simon Bliudze [email protected] Eduard Baranov [email protected]
1
Université catholique de Louvain, Place de l’Université 1, 1348 Ottignies-Louvain-la-Neuve, Belgium
2
INRIA Lille – Nord Europe, 40 avenue Halley, 59650 Villeneuve d’Ascq, France
123
E. Baranov, S. Bliudze
BIP is a component-based framework for the design of concurrent systems based on the separation of concerns between coordination and computation [6,7]. It is among the few frameworks, such as SCADE [15] and Ptolemy II [20], which combine the use of formal methods for defining their operational semantics and for model verification, with code generation. Recently we have developed a theory of architectures [1,2], which allows the compositional design of correct-by-construction BIP models. This theory formalises BIP design patterns, called architectures. The application of an architecture to a BIP system enforces the corresponding characteristic property. We have shown that safety properties are preserved by composition of architectures and have provided an algorithm for verifying whether two architectures are non-interfering, which gua
Data Loading...
