A Composition Mechanism for Refinement-Based Methods

被引：18

作者：

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 条

[41] 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
[42] A refinement-based approach to safe smart contract deployment and evolution
Antonino, Pedro
Ferreira, Juliandson
Sampaio, Augusto
Roscoe, A. W.
Arruda, Filipe
SOFTWARE AND SYSTEMS MODELING, 2024, 23 (03): : 657 - 693
[43] A Case Study in Refinement-Based Modelling of a Resilient Control System
Prokhorova, Yuliya
Troubitsyna, Elena
Laibinis, Linas
SOFTWARE ENGINEERING FOR RESILIENT SYSTEMS, SERENE 2013, 2013, 8166 : 79 - 93
[44] Refinement-based requirements modeling using Triggered Message Sequence Charts
Sengupta, B
Cleaveland, R
11TH IEEE INTERNATIONAL REQUIREMENTS ENGINEERING CONFERENCE, PROCEEDINGS, 2003, : 95 - 104
[45] Formal Proofs of Termination Detection for Local Computations by Refinement-Based Compositions
Boussabbeh, Maha
Tounsi, Mohamed
Mosbah, Mohamed
Kacem, Ahmed Hadj
ABSTRACT STATE MACHINES, ALLOY, B, TLA, VDM, AND Z (ABZ 2016), 2016, 9675 : 198 - 212
[46] Reusable component IP design using refinement-based design environment
Park, Sanggyu
Yoon, Sangyong
Chae, Soo-Ik
ASP-DAC 2006: 11TH ASIA AND SOUTH PACIFIC DESIGN AUTOMATION CONFERENCE, PROCEEDINGS, 2006, : 588 - 593
[47] A New Receiver Placement Scheme Using Delaunay Refinement-based Triangulation
Basheer, Mohammed Rana
Jagannathan, S.
2010 IEEE WIRELESS COMMUNICATIONS AND NETWORKING CONFERENCE (WCNC 2010), 2010,
[48] Refinement-Based Modeling and Formal Verification for Multiple Secure Partitions of TrustZone
Zeng F.-L.
Chang R.
Xu H.
Pan S.-P.
Zhao Y.-W.
Ruan Jian Xue Bao/Journal of Software, 2023, 34 (08):
[49] Refinement-based disintegration: An approach to re-representation in relational learning
Ontanon, Santiago
Plaza, Enric
AI COMMUNICATIONS, 2015, 28 (01) : 35 - 46
[50] LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs
Qiu, Longfei
Kim, Yoonseung
Shin, Ji-Yong
Kim, Jieung
Honore, Wolf
Shao, Zhong
PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2024, 8 (PLDI): : 1140 - 1164

← 1 2 3 4 5 →