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 条

[41] From Object-Z specification to Groovy implementation
Zaker, F.
Haghighi, H.
Nazemi, E.
SCIENTIA IRANICA, 2018, 25 (06) : 3415 - 3441
[42] Verification of Object-Z specifications by using transition systems: Application to the radiomobile network design problem
Gruer, P
Hilaire, V
Koukam, A
FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING, 2000, 1783 : 222 - 236
[43] 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
[44] 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
[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+58
[49] Formal specification of CORBA services using Object-Z
Kreuz, D
SECOND INTERNATIONAL CONFERENCE ON FORMAL ENGINEERING METHODS, PROCEEDINGS, 1998, : 180 - 189
[50] 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

← 1 2 3 4 5 →