Structural refinement in Object-Z/CSP

被引:0
|
作者
Derrick, J [1 ]
Smith, G
机构
[1] Univ Kent, Comp Lab, Canterbury CT2 7NF, Kent, England
[2] Univ Queensland, Software Verificat Res Ctr, St Lucia, Qld 4072, Australia
来源
关键词
D O I
暂无
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
State-based refinement relations have been developed for use on the Object-Z components in an integrated Object-Z / CSP specification. However this refinement methodology does not allow the structure of a specification to be changed in a refinement, whereas a full methodology would allow concurrency to be introduced during the development life-cycle. In this paper we tackle these concerns and discuss refinements of specifications written using Object-Z and CSP where we change the structure of the specification when performing the refinement. In particular, we develop a set of structural simulation rules which allow a single Object-Z component to be refined to a number of communicating or interleaved classes. We prove soundness of these rules and illustrate them with a small example.
引用
收藏
页码:194 / 213
页数:20
相关论文
共 50 条
  • [31] Translating fusion/UML to Object-Z
    Bittner, M
    Kammüller, F
    FIRST ACM AND IEEE INTERNATIONAL CONFERENCE ON FORMAL METHODS AND MODELS FOR CO-DESIGN, PROCEEDINGS, 2003, : 49 - 50
  • [32] Animation of object-Z specifications using a Z animator
    McComb, T
    Smith, G
    FIRST INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND FORMAL METHODS, PROCEEDINGS, 2003, : 191 - 200
  • [33] 一种从Object-Z到CSP规格说明的转化方法
    文志诚
    缪淮扣
    许庆国
    计算机科学, 2006, (11) : 263 - 267
  • [34] Structured object-Z software specification language
    Gao, XL
    Miao, HK
    Chen, YH
    GRID AND COOPERATIVE COMPUTING, PT 1, 2004, 3032 : 956 - 963
  • [35] 使用Object-Z获取形式需求
    朱彬
    王帅
    王娜
    计算机辅助工程, 2008, (01) : 87 - 90
  • [36] Formalizing semantics of XSLT using Object-Z
    Yang, HL
    Dong, JS
    Hao, KG
    Han, JG
    WEB TECHNOLOGIES AND APPLICATIONS, 2003, 2642 : 120 - 131
  • [37] Modelling Java']Java concurrency with object-Z
    Duke, R
    Wildman, L
    Long, B
    FIRST INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND FORMAL METHODS, PROCEEDINGS, 2003, : 173 - 181
  • [38] A minimal set of refactoring rules for Object-Z
    McComb, Tim
    Smith, Graeme
    FORMAL METHODS FOR OPEN OBJECT-BASED DISTRIBUTED SYSTEMS, PROCEEDINGS, 2008, 5051 : 170 - +
  • [39] Viewpoints and consistency: translating LOTOS to Object-z
    Derrick, J
    Boiten, E
    Bowman, H
    Steen, M
    COMPUTER STANDARDS & INTERFACES, 1999, 21 (03) : 251 - 272
  • [40] Understanding object-Z operations as generalised substitutions
    Dunne, S
    INTEGRATED FORMAL METHODS, PROCEEDINGS, 2004, 2999 : 328 - 342