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 条
  • [31] 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
  • [32] 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
  • [33] Structured object-Z software specification language
    Gao, XL
    Miao, HK
    Chen, YH
    GRID AND COOPERATIVE COMPUTING, PT 1, 2004, 3032 : 956 - 963
  • [34] 使用Object-Z获取形式需求
    朱彬
    王帅
    王娜
    计算机辅助工程, 2008, (01) : 87 - 90
  • [35] Formalizing semantics of XSLT using Object-Z
    Yang, HL
    Dong, JS
    Hao, KG
    Han, JG
    WEB TECHNOLOGIES AND APPLICATIONS, 2003, 2642 : 120 - 131
  • [36] 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
  • [37] 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 - +
  • [38] Viewpoints and consistency: translating LOTOS to Object-z
    Derrick, J
    Boiten, E
    Bowman, H
    Steen, M
    COMPUTER STANDARDS & INTERFACES, 1999, 21 (03) : 251 - 272
  • [39] Understanding object-Z operations as generalised substitutions
    Dunne, S
    INTEGRATED FORMAL METHODS, PROCEEDINGS, 2004, 2999 : 328 - 342
  • [40] FOOM: A diagrammatic illustration of Object-Z specifications
    Wafula, EN
    Swatman, PA
    OBJECT ORIENTED SYSTEMS, 1996, 3 (04): : 215 - 242
12345