Ozkaya, M. & Kloukinas, C. (2014). Design-by-contract for reusable components and realizable architectures. In: CBSE '14 Proceedings of the 17th international ACM Sigsoft symposium on Component-based software engineering. (pp. 129-138). New York, USA: ACM. ISBN 9781450325776
- Accepted Version
Download (322kB) | Preview
Architectural connectors can increase the modularity and reusability benefits of Component-based Software Engineering, as they allow one to specify the general case of an interaction pattern and reuse it from then on. At the same time they enable components to be protocol-independent – components do not need to know under which interaction patterns they will be used, as long as their minimal, local interaction constraints are satisfied. Without connectors one can specify only specific instances of such patterns and components need to specify themselves the interaction protocols that they will follow, thus reducing their reusability.
Connector frameworks so far allow designers to specify systems that are unrealizable in a decentralized manner, as they allow designers to impose global interaction constraints. These frameworks either ignore the realizability problem altogether, ignore connector behaviour when generating code, or introduce a centralized controller that enforces these global constraints but does so at the price of invalidating any decentralized properties of the architecture.
We show how the XCD ADL extends Design-by-Contract (DbC) for specifying (i) protocol-independent components, and (ii) arbitrary connectors that are always realizable in a decentralized manner as specified by an architecture – XCD connectors impose local constraints only. Use of DbC will hopefully make it easier for practitioners to use the language, compared to languages using process algebras. We show how XCD specifications can be translated to ProMeLa so as to verify that (i) provided services local interaction constraints are satisfied, (ii) provided services functional pre-conditions are complete, (iii) there are no race-conditions, (iv) event buffer sizes suffice, and (v) there is no global deadlock. Without formally analyzable architectures errors can remain undiscovered for a long time and cost too much to repair.
|Item Type:||Book Section|
|Additional Information:||© Mert Ozkaya| ACM 2014. This is the author's version of the work. It is posted here for your personal use. Not for redistribution. The definitive Version of Record was published in CBSE '14 Proceedings of the 17th international ACM Sigsoft symposium on Component-based software engineering, http://dx.doi.org/10.1145/10.1145/2602458.2602463|
|Uncontrolled Keywords:||Modular specifications, Separation of functional and interaction behaviours, Connector realizability|
|Subjects:||Q Science > QA Mathematics > QA75 Electronic computers. Computer science|
|Divisions:||School of Informatics > Department of Computing|
Actions (login required)
Downloads per month over past year