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 条
  • [21] Refinement-Based CFG Reconstruction from Unstructured Programs
    Bardin, Sebastien
    Herrmann, Philippe
    Vedrine, Franck
    VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, 2011, 6538 : 54 - 69
  • [22] Refinement-based verification of sequential implementations of Stateflow charts
    Miyazawa, Alvaro
    Cavalcanti, Ana
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2011, (55): : 65 - 83
  • [23] Refinement-Based Similarity Measures for Directed Labeled Graphs
    Ontanon, Santiago
    Shokoufandeh, Ali
    CASE-BASED REASONING RESEARCH AND DEVELOPMENT, ICCBR 2016, 2016, 9969 : 311 - 326
  • [24] Refinement-based Exact Response-Time Analysis
    Stigge, Martin
    Guan, Nan
    Yi, Wang
    2014 26TH EUROMICRO CONFERENCE ON REAL-TIME SYSTEMS (ECRTS 2014), 2014, : 143 - 152
  • [25] Modeling security as a dependability attribute: a refinement-based approach
    Mili, Ali
    Sheldon, Frederick
    Jilani, Lamia Labed
    Vinokurov, Alex
    Thomasian, Alex
    Ben Ayed, Rahma
    INNOVATIONS IN SYSTEMS AND SOFTWARE ENGINEERING, 2006, 2 (01) : 39 - 48
  • [26] Refinement-Based Specification and Security Analysis of Separation Kernels
    Zhao, Yongwang
    Sanan, David
    Zhang, Fuyuan
    Liu, Yang
    IEEE TRANSACTIONS ON DEPENDABLE AND SECURE COMPUTING, 2019, 16 (01) : 127 - 141
  • [27] Refinement-Based Game Semantics for Certified Abstraction Layers
    Koenig, Jeremie
    Shao, Zhong
    PROCEEDINGS OF THE 35TH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS 2020), 2020, : 633 - 647
  • [28] Refinement-Based OWL Class Induction with Convex Measures
    Ratcliffe, David
    Taylor, Kerry
    SEMANTIC TECHNOLOGY, JIST 2017, 2017, 10675 : 49 - 65
  • [29] Refinement-based Validation of Event-B Specifications
    Mashkoor, Atif
    Yang, Faqing
    Jacquot, Jean-Pierre
    SOFTWARE AND SYSTEMS MODELING, 2017, 16 (03): : 789 - 808
  • [30] A membership degree refinement-based evolutionary clustering algorithm
    Hou, Wei
    Dong, Hongbin
    Yin, Guisheng
    Jisuanji Yanjiu yu Fazhan/Computer Research and Development, 2013, 50 (03): : 548 - 558
12345