Malaysian Journal of Computer Science (ISSN 0127-9084)
Indexing Page
Visit the official web site at

Article Information
Title:Formal Verification of Contractual Software Architectures using SPIN
Auhtor(s): Mert Ozkaya,
Journal:Malaysian Journal of Computer Science (ISSN 0127-9084)
Volume:28, No 4
Keywords:software architectures, formal verification, SPIN, design-by-contract
Abstract:Software architectures have become one of the most crucial aspects of software engineering. Software architectures let designers specify systems in terms of components and their relations (i.e., connectors). These components along with their relations can then be verified to check whether their behaviours meet designersí expectations. XCD is a novel architecture description language, which promotes contractual specification of software architectures and their automated formal verifications in SPIN. XCD allows designers to formally verify their system specifications for a number of properties, i.e., (i) incomplete functional behaviour of components, (ii) wrong use of services operated by system components, (iii) deadlock, (iv) race-conditions, and (v) buffer overflows in the case of asynchronous (i.e., event-based) communications. In addition to these properties, designers can specify their own properties in linear temporal logic and check their correctness. In this paper, I discuss XCD and its support for formal verification of software architectures through a simple shared-data access case study.

Volume Listing