City Research Online

Abstract

Design-by-Contract (DbC) gained wide familiarity among software developers for specifying software. It aids in documenting the behaviour of class methods as contracts between clients of the methods (pre-) and their suppliers (post-condition). This not only allows developers to document software behaviour precisely at such a high-level that can more easily be communicated, but also enables the formal verification of the behaviour.

In this paper, we provide a comprehensive extension to DbC so that it can also be applied to the level of software architecture design. We illustrate this through our architecture description language XCD. Components in XCD have four different types of interfaces: provided and required interfaces of methods or emitter and consumer interfaces of events where methods/events are contractually specified. Contract specification is separated into functional and interaction contracts thus modularising the functional and interaction component behaviours. Furthermore, treating interaction protocols as connectors, XCD allows to specify connectors with interaction contracts that participating components adhere to.

The formal semantics of XCD are defined using Finite State Process (FSP) thus enabling formal analysis of contractually specified software architectures for quality properties, e.g., deadlock.

Publication Type:	Conference or Workshop Item (Paper)
Additional Information:	© 2013 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.
Subjects:	Q Science > QA Mathematics > QA76 Computer software
Departments:	School of Science & Technology > Computer Science
Related URLs:	Publisher

Export

Downloads