Visual Specification and Analysis of Contract-Based Software Architectures

XCD is a design-by-contract based architecture description language that supports modular specifications in terms of components and connectors (i.e., interaction protocols). XCD is supported by a translator that produces formal models in SPIN's ProMeLa formal verification language, which can then be formally analysed using SPIN's model checker. XCD is extended with a visual notation set called VXCD. VXCD extends UML's component diagram and adapts it to XCD's structure, contractual behaviour, and interaction protocol specifications. Visual VXCD specifications can be translated into textual XCD specifications for formal analysis. To illustrate VXCD, the well-known gas station system is used. The gas system is specified contractually using VXCD's visual notation set and then formally analysed using SPIN's model checker for a number of properties including deadlock and race-condition.