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 条
  • [41] FOOM: A diagrammatic illustration of Object-Z specifications
    Wafula, EN
    Swatman, PA
    OBJECT ORIENTED SYSTEMS, 1996, 3 (04): : 215 - 242
  • [42] From Object-Z specification to Groovy implementation
    Zaker, F.
    Haghighi, H.
    Nazemi, E.
    SCIENTIA IRANICA, 2018, 25 (06) : 3415 - 3441
  • [43] An Instance to Extend Object-Z Formal Specification
    Hou, Xiaomao
    Ma, Ling
    Wen, Zhicheng
    ADVANCES IN MECHATRONICS, AUTOMATION AND APPLIED INFORMATION TECHNOLOGIES, PTS 1 AND 2, 2014, 846-847 : 1500 - 1504
  • [44] Translating the OMT dynamic model into Object-Z
    Dupuy, S
    Ledru, Y
    Chabre-Peccoud, M
    ZUM '98: THE Z FORMAL SPECIFICATION NOTATION, 1998, 1493 : 347 - 366
  • [45] Viewpoints and consistency: Translating LOTOS to Object-Z
    Derrick, John
    Boiten, Eerke
    Bowman, Howard
    Steen, Maarten
    Computer Standards and Interfaces, 1999, 21 (03): : 251 - 272
  • [46] Translating Object-Z specifications to object-oriented test oracles
    McDonald, J
    Murray, L
    Strooper, P
    ASIA PACIFIC SOFTWARE ENGINEERING CONFERENCE AND INTERNATIONAL COMPUTER SCIENCE CONFERENCE, PROCEEDINGS, 1997, : 414 - 423
  • [47] Comparison of formalisation approaches of UML class constructs in Z and Object-Z
    Amálio, N
    Polack, F
    ZB 2003: FORMAL SPECIFICATION AND DEVELOPMENT IN Z AND B, 2003, 2651 : 339 - 358
  • [48] Object-Z规格到实现机制探讨
    王志刚
    谢茂芳
    计算机光盘软件与应用, 2013, 16 (21) : 59 - 61
  • [49] Extending Linear Temporal Logic With Clocks to Object-Z
    Wen, Zhicheng
    Chen, Zhigang
    APPLIED SCIENCE, MATERIALS SCIENCE AND INFORMATION TECHNOLOGIES IN INDUSTRY, 2014, 513-517 : 927 - 930
  • [50] Formal specification of CORBA services using Object-Z
    Kreuz, D
    SECOND INTERNATIONAL CONFERENCE ON FORMAL ENGINEERING METHODS, PROCEEDINGS, 1998, : 180 - 189