A Composition Mechanism for Refinement-Based Methods

被引：16

作者：

Hoang, Thai Son ^{[1
]}

Dghaym, Dana ^{[1
]}

Snook, Colin ^{[1
]}

Butler, Michael ^{[1
]}

机构：

[1] Univ Southampton, Elect & Comp Sci, Southampton, Hants, England

来源：

2017 22ND INTERNATIONAL CONFERENCE ON ENGINEERING OF COMPLEX COMPUTER SYSTEMS (ICECCS) | 2017年

基金：

欧盟地平线“2020”;

关键词：

Machine Inclusion; Composition; Refinement; Event-B; EVENT-B; MODELS; INSTANTIATION;

D O I：

10.1109/ICECCS.2017.27

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

Event-B developments are mostly structured around the refinement relationship. This top-down development architecture enables system details to be gradually introduced into the formal model. However, this results in large models with monolithic structures. We develop a composition mechanism allowing to develop models bottom-up. In particular, our proposed mechanism works seamlessly with the existing refinement technique in Event-B. As a result we have built a formal development method that can take advantage of both top-down and bottom-up approaches. We prove the correctness of machine inclusion with refinement using the supporting Rodin platform.

引用

页码：100 / 109

页数：10

共 50 条

[31] Optimal Refinement-based Array Constraint Solving for Symbolic Execution
Liu, Meixi
Shuai, Ziqi
Liu, Luyao
Ma, Kelin
Ma, Ke
2022 29TH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE, APSEC, 2022, : 299 - 308
[32] Refinement-Based Verification of Interactive Real-Time Systems
Spichkova, Maria
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2008, 214 : 131 - 157
[33] REBA: A Refinement-Based Architecture for Knowledge Representation and Reasoning in Robotics
Sridharan, Mohan
Gelfond, Michael
Zhang, Shiqi
Wyatt, Jeremy
JOURNAL OF ARTIFICIAL INTELLIGENCE RESEARCH, 2019, 65 : 87 - 180
[34] THETA: a Framework for Abstraction Refinement-Based Model Checking
Toth, Tamas
Hajdu, Akos
Voros, Andras
Micskei, Zoltan
Majzik, Istvan
PROCEEDINGS OF THE 17TH CONFERENCE ON FORMAL METHODS IN COMPUTER AIDED DESIGN (FMCAD 2017), 2017, : 176 - 179
[35] Refinement-based verification for possibly-cyclic lists
Loginov, Alexey
Reps, Thomas
Sagiv, Mooly
PROGRAM ANALYSIS AND COMPILATION, THEORY AND PRACTICE: ESSAYS DEDICATED TO REINHARD WILHELM ON THE OCCASION OF HIS 60TH BIRTHDAY, 2007, 4444 : 247 - +
[36] A refinement-based compositional reasoning framework for pipelined machine verification
Manolios, Panagiotis
Srinivasan, Sudarshan K.
IEEE TRANSACTIONS ON VERY LARGE SCALE INTEGRATION (VLSI) SYSTEMS, 2008, 16 (04) : 353 - 364
[37] Local extrema refinement-based tensor product model transformation controller with problem independent sampling methods
Chang, Fei
Shi, Bao
Li, Xin
Zhao, Guoliang
Huang, Sharina
ASIAN JOURNAL OF CONTROL, 2021, 23 (03) : 1352 - 1366
[38] A Refinement-Based Correctness Proof of Symmetry Reduced Model Checking
Turner, Edd
Butler, Michael
Leuschel, Michael
ABSTRACT STATE MACHINES, ALLOY, B AND Z, PROCEEDINGS, 2010, 5977 : 231 - +
[39] A Refinement-Based Approach for Proving Distributed Algorithms on Evolving Graphs
Fakhfakh, Faten
Tounsi, Mohamed
Kacem, Ahmed Hadj
Mosbah, Mohamed
2016 IEEE 25TH INTERNATIONAL CONFERENCE ON ENABLING TECHNOLOGIES: INFRASTRUCTURE FOR COLLABORATIVE ENTERPRISES (WETICE), 2016, : 44 - 49
[40] Crafting data structures: A study of reference locality in refinement-based pathfinding
Niewiadomski, R
Amaral, JN
Holte, RC
HIGH PERFORMANCE COMPUTING - HIPC 2003, 2003, 2913 : 438 - 448

← 1 2 3 4 5 →