Rigorous development of component-based systems using component metadata and patterns

In previous work we presented a CSP-based systematic approach that fosters the rigorous design of component-based development. Our approach is strictly defined in terms of composition rules, which are the only permitted way to compose components. These rules guarantee the preservation of properties...

Full description

Saved in:
Bibliographic Details
Published in:Formal aspects of computing 2016-11, Vol.28 (6), p.937-1004
Main Authors: Oliveira, M. V. M., Antonino, P., Ramos, R., Sampaio, A., Mota, A., Roscoe, A. W.
Format: Article
Language:English
Subjects:
Algorithms
Behavioural
Computer Science
Design analysis
Design engineering
Leadership
Math Applications in Computer Science
Metadata
Original Article
Running
Theory of Computation
Topology
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:In previous work we presented a CSP-based systematic approach that fosters the rigorous design of component-based development. Our approach is strictly defined in terms of composition rules, which are the only permitted way to compose components. These rules guarantee the preservation of properties (particularly deadlock freedom) by construction in component composition. Nevertheless, their application is allowed only under certain conditions whose verification via model checking turned out impracticable even for some simple designs, and particularly those involving cyclic topologies. In this paper, we address the performance of the analysis and present a significantly more efficient alternative to the verification of the rule side conditions, which are improved by carrying out partial verification on component metadata throughout component compositions and by using behavioural patterns. The use of metadata, together with behavioural patterns, demands new composition rules, which allow previous exponential time verifications to be carried out now in linear time. Two case studies (the classical dining philosophers, also used as a running example, and an industrial version of a leadership election algorithm) are presented to illustrate and validate the overall approach.
ISSN:0934-5043
1433-299X
DOI:10.1007/s00165-016-0375-1