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 条
  • [41] 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
  • [42] 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
  • [43] Refinement-based requirements modeling using Triggered Message Sequence Charts
    Sengupta, B
    Cleaveland, R
    11TH IEEE INTERNATIONAL REQUIREMENTS ENGINEERING CONFERENCE, PROCEEDINGS, 2003, : 95 - 104
  • [44] 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
  • [45] 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
  • [46] 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
  • [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 disintegration: An approach to re-representation in relational learning
    Ontanon, Santiago
    Plaza, Enric
    AI COMMUNICATIONS, 2015, 28 (01) : 35 - 46
  • [49] 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):
  • [50] Preserving languages and properties in stepwise refinement-based synthesis of Petri nets
    Ding, ZhiJun
    Jiang, ChangJun
    Zhou, MengChu
    Zhang, YaYing
    IEEE TRANSACTIONS ON SYSTEMS MAN AND CYBERNETICS PART A-SYSTEMS AND HUMANS, 2008, 38 (04): : 791 - 801
12345