? 基于契约的软件结构的可视化规范与分析
Journal of Computer Science and Technology
Quick Search in JCST
 Advanced Search 
      Home | PrePrint | SiteMap | Contact Us | Help
 
Indexed by   SCIE, EI ...
Bimonthly    Since 1986
Journal of Computer Science and Technology 2017, Vol. 32 Issue (5) :1025-1043    DOI: 10.1007/s11390-017-1779-y
Regular Paper << Previous Articles | Next Articles >>
基于契约的软件结构的可视化规范与分析
Mert Ozkaya
Department of Computer Engineering, Istanbul Kemerburgaz University, Istanbul 34217, Turkey
Visual Specification and Analysis of Contract-Based Software Architectures
Mert Ozkaya
Department of Computer Engineering, Istanbul Kemerburgaz University, Istanbul 34217, Turkey

摘要
参考文献
相关文章
Download: [PDF 5929KB]  
摘要 XCD是一种基于契约设计的结构描述语言,该语言以组件和连接器(即,交互协议)的形式支持模块化的规约。XCD由一个翻译器支持,该翻译器能生成用SPIN的ProMeLa形式验证语言描述的形式化模型,该模型能使用SPIN的模型检查器进行形式化的验证。VXCD是XCD基于一个可视化标记集合的扩展。VXCD扩展了UML的组件图,并使之与XCD的结构、合同行为和交互协议规范相适应。可视化VXCD规范可以转换为可用于形式化分析的文本XCD规范。为说明VXCD,本文使用了众所周知的Gas Station系统。首先,使用VXCD可视化符号集描述了该系统;接着,使用SPIN的模型检查器,形式化地验证了大量属性,例如:死锁和竞争条件。
关键词结构化语言   契约式设计   可视化建模语言   交互协议   形式化分析     
Abstract: 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.
Keywordsarchitectural language   design-by-contract   visual modelling language   interaction protocol   formal analysis     
Received 2016-09-14;
本文基金:

This work was supported by the Project of the Scientific and Technological Research Council of Turkey (TUBITAK) under Grant No. 215E159.

About author: Mert Ozkaya is assistant professor in Istanbul Kemerburgaz University, Istanbul. Dr. Ozkaya received his Ph.D. degree in computer science from City University London, London, in 2014. Previously, he received his M.S. degree in computer science from University of Essex, Colchester, in 2010, and his B.S. degree in computer engineering from Bilkent University, Ankara, in 2009.
引用本文:   
Mert Ozkaya.基于契约的软件结构的可视化规范与分析[J]  Journal of Computer Science and Technology , 2017,V32(5): 1025-1043
Mert Ozkaya.Visual Specification and Analysis of Contract-Based Software Architectures[J]  Journal of Computer Science and Technology, 2017,V32(5): 1025-1043
链接本文:  
http://jcst.ict.ac.cn:8080/jcst/CN/10.1007/s11390-017-1779-y
Copyright 2010 by Journal of Computer Science and Technology