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 条
  • [21] Formalizing UML models with object-Z
    Miao, HK
    Liu, L
    Li, L
    FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS, 2002, 2495 : 523 - 534
  • [22] Integrating Object-Z with Timed Automata
    Dong, JS
    Duke, R
    Hao, P
    ICECCS 2005: 10TH IEEE INTERNATIONAL CONFERENCE ON ENGINEERING OF COMPLEX COMPUTER SYSTEMS, PROCEEDINGS, 2005, : 488 - 497
  • [23] Static Class Elements for Object-Z
    Ruhroth, Thomas
    Wehrheim, Heike
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2009, 259 (0C) : 193 - 205
  • [24] Abstract specification in object-Z and CSP
    Smith, G
    Derrick, J
    FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS, 2002, 2495 : 108 - 119
  • [25] Formalizing object oriented design patterns with object-Z
    Rauf, Irum
    Nadeem, Aamer
    Khokhar, Masud
    10TH IEEE INTERNATIONAL MULTITOPIC CONFERENCE 2006, PROCEEDINGS, 2006, : 269 - +
  • [26] Implementing Object-Z with Perfect Developer
    Stevens, Brian
    JOURNAL OF OBJECT TECHNOLOGY, 2006, 5 (02): : 189 - 202
  • [27] Polymorphic extensions to Object-Z specifications
    Waheed, Tabinda
    Khan, Muhammad Uzair
    Nadeem, Aamer
    TENCON 2006 - 2006 IEEE REGION 10 CONFERENCE, VOLS 1-4, 2006, : 1971 - 1974
  • [28] Mutation operators for Object-Z specification
    Liu, L
    Miao, HK
    ICECCS 2005: 10TH IEEE INTERNATIONAL CONFERENCE ON ENGINEERING OF COMPLEX COMPUTER SYSTEMS, PROCEEDINGS, 2005, : 498 - 506
  • [29] Structural refinement in Object-Z/CSP
    Derrick, J
    Smith, G
    INTEGRATED FORMAL METHODS, PROCEEDINGS, 2000, 1945 : 194 - 213
  • [30] 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
12345