LORIA (Vandoeuvre-lès-Nancy, FRANCE)
PRISM (University of Versailles St-Quentin, FRANCE)
CADP (Construction and Analysis of Distributed Processes)
about 300000 states and 1500000 transitions
The specification of the architecture is an important step in the life
cycle of a software system. This is done by specifying the desired
behaviour of the system in terms of components and
connectors. Architectural styles are used in order to
facilitate the identification and definition of high-quality
components and connectors. An architectural style consists of five
parts: a set of components and connectors, the former
representing computation or data entities and the latter modelling
the interactions between components; a global configuration,
which describes the architectural structure characteristic to the
style, i.e., a scheme representing the interaction pattern between
components and connectors and the general behaviour of a specification;
a set of characteristics, which encompass all parameters of the
style, i.e., all information necessary to define a specification by
instantiating a particular scheme; a set of architectural
constraints, which are the properties that a specification must
meet in order to belong to a given style; and a set of
variations, which are schemes describing various definitions of
components and connectors that preserve the behaviour of the system.
In the architectural style Pipe and Filter, each component acts as a filter, i.e., it has a set of inputs and a set of outputs on which it reads and produces data flows, and each connector behaves as a pipe, i.e., it connects the outputs of a filter to the inputs of other filters. Filters are independent entities (do not share data). This architectural style has been formally described in LOTOS by encoding filters and pipes as LOTOS processes connected by gates. The global configuration of a system is encoded by a LOTOS behaviour expression parameterized by the attributes characteristic to the style, and which must satisfy a set of architectural constraints. Variations on this style are modelled as different specification solutions for filters and pipes that must preserve the safety equivalence of Pipe and Filter specifications.
This approach has been experimented on a systolic array implementing the convolution product. The array cells are represented by filters that communicate through pipes and are connected in pipeline. A special broadcast filter is used to supply input values to the other filters. Several variations of the specification, obtained by using different types of filters (blocking, non-blocking) and pipes (simple, bounded, unbounded) have been experimented and analysed using the CADP toolset. This enabled to check that all variations obtained on the LOTOS specification are safety equivalent.
Formal descriptions of architectural styles provide the only way to
precisely answer design questions about the set of system components,
their behaviour, and their interconnections. The LOTOS language has
been found appropriate for the description of architectural styles,
by allowing to define parameterized specification schemes that can be
instantiated in order to develop software architectures belonging to
a given style. In addition, the software design is facilitated by the
availability of existing verification toolsets, such as CADP.
S. Rongviriyapanish and N. Lévy.
"Variations sur le style architectural Pipe & Filter".
In P. Berlioux and Y. Ledru, editors, Actes du 3eme Colloque sur les
Approches Formelles dans l'Assistance au Développement de
Logiciels AFADL'2000 (Grenoble, France), pp. 81-95, ADER and LSR-IMAG,
Available on-line at: http://www-lsr.imag.fr/afadl/Programme/Articles/levy.ps
or also from the CADP Web site in PDF or PostScript
54506 Vandoeuvre-lès-Nancy Cedex
Tel: +33 (0)3 83 59 20 42
Fax: +33 (0)3 83 41 30 79
|This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies