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 条
  • [1] Refinement and verification of concurrent systems specified in Object-Z and CSP
    Smith, G
    Derrick, J
    FIRST IEEE INTERNATIONAL CONFERENCE ON FORMAL ENGINEERING METHODS, PROCEEDINGS, 1997, : 293 - 302
  • [2] Timed CSP and Object-Z
    Derrick, J
    ZB 2003: FORMAL SPECIFICATION AND DEVELOPMENT IN Z AND B, 2003, 2651 : 300 - 318
  • [3] Specification, Refinement and Verification of Concurrent Systems—An Integration of Object-Z and CSP
    Graeme Smith
    John Derrick
    Formal Methods in System Design, 2001, 18 : 249 - 284
  • [4] Specification, refinement and verification of concurrent systems - An integration of Object-Z and CSP
    Smith, G
    Derrick, J
    FORMAL METHODS IN SYSTEM DESIGN, 2001, 18 (03) : 249 - 284
  • [5] Abstract specification in object-Z and CSP
    Smith, G
    Derrick, J
    FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS, 2002, 2495 : 108 - 119
  • [6] Compositional class refinement in Object-Z
    McComb, Tim
    Smith, Graeme
    FM 2006: FORMAL METHODS, PROCEEDINGS, 2006, 4085 : 205 - 220
  • [7] Refinement of objects and operations in Object-Z
    Derrick, J
    Boiten, E
    FORMAL METHODS FOR OPEN OBJECT-BASED DISTRIBUTED SYSTEMS IV, 2000, 49 : 257 - 277
  • [8] Blending Object-Z and Timed CSP: An introduction to TCOZ
    Mahony, B
    Dong, JS
    PROCEEDINGS OF THE 1998 INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING, 1998, : 95 - 104
  • [9] A case study in partial specification: Consistency and refinement for object-Z
    Taylor, C
    Derrick, J
    Boiten, E
    ICFEM 2000: THIRD INTERNATIONAL CONFERENCE ON FORMAL ENGINEERING METHODS, PROCEEDINGS, 2000, : 177 - 185
  • [10] UML/OCL or Object-Z?
    Bettaz, Mohamed
    Maouche, Mourad
    2017 INTERNATIONAL CONFERENCE ON INFOCOM TECHNOLOGIES AND UNMANNED SYSTEMS (TRENDS AND FUTURE DIRECTIONS) (ICTUS), 2017, : 78 - 83