Compositional verification for Object-Z

被引：0
|
作者：
Winter, K [1 ]
Smith, G [1 ]
机构：
[1] Univ Queensland, Software Verificat Res Ctr, Brisbane, Qld 4072, Australia
来源：
ZB 2003: FORMAL SPECIFICATION AND DEVELOPMENT IN Z AND B | 2003年 / 2651卷
关键词：
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
This paper presents a framework for compositional verification of Object-Z specifications. Its key feature is a proof rule based on decomposition of hierarchical Object-Z models. For each component in the hierarchy local properties are proven in a single proof step. However, we do not consider components in isolation. Instead, components are envisaged in the context of the referencing super-component and proof steps involve assumptions on properties of the sub-components. The framework is defined for Linear Temporal Logic (LTL).
引用
收藏
页码：280 / 299
页数：20
相关论文
共 50 条
  • [1] Compositional class refinement in Object-Z
    McComb, Tim
    Smith, Graeme
    FM 2006: FORMAL METHODS, PROCEEDINGS, 2006, 4085 : 205 - 220
  • [2] Slicing Object-Z specifications for verification
    Brückner, I
    Wehrheim, H
    ZB 2005: FORMAL SPECIFICATION AND DEVELOPMENT IN Z AND B, PROCEEDINGS, 2005, 3455 : 414 - 433
  • [3] 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
  • [4] 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
  • [5] Heterogeneous formal specification based on Object-Z and statecharts: semantics and verification
    Gruer, JP
    Hilaire, V
    Koukam, A
    Rovarini, P
    JOURNAL OF SYSTEMS AND SOFTWARE, 2004, 70 (1-2) : 95 - 105
  • [6] 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
  • [7] 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
  • [8] Modular reasoning in Object-Z
    Griffiths, A
    ASIA PACIFIC SOFTWARE ENGINEERING CONFERENCE AND INTERNATIONAL COMPUTER SCIENCE CONFERENCE, PROCEEDINGS, 1997, : 140 - 149
  • [9] Timed CSP and Object-Z
    Derrick, J
    ZB 2003: FORMAL SPECIFICATION AND DEVELOPMENT IN Z AND B, 2003, 2651 : 300 - 318
  • [10] Refactoring object-Z specifications
    McComb, T
    FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING, PROCEEDINGS, 2004, 2984 : 69 - 83
12345