We use cookies to improve your experience with our site.
Mert Ozkaya. Visual Specification and Analysis of Contract-Based Software Architectures[J]. Journal of Computer Science and Technology, 2017, 32(5): 1025-1043. DOI: 10.1007/s11390-017-1779-y
Citation: Mert Ozkaya. Visual Specification and Analysis of Contract-Based Software Architectures[J]. Journal of Computer Science and Technology, 2017, 32(5): 1025-1043. DOI: 10.1007/s11390-017-1779-y

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.
  • loading

Catalog

    /

    DownLoad:  Full-Size Img  PowerPoint
    Return
    Return