Refinement for Pipelining in Event-B

被引：0
|
作者：
Evans, Neil [1 ]
机构：
[1] AWE, Aldermaston, England
来源：
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE | 2008年 / 214卷
关键词：
Refinement; Event-B; pipelined architecture;
D O I：
10.1016/j.entcs.2008.06.009
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
The refinement of an implementation-independent specification of an instruction set to a simple pipelined architecture is presented to illustrate subtleties in the formal development and analysis of pipelined hardware from such specifications. The Event-B language and its tool support (the Eclipse-based Rodin platform) is used for this purpose. The example demonstrates that naive use of Event-B's superposition refinement fails to expose all of the potential hazards in pipelining. This paper introduces a form of 'event merging' to complete the analysis.
引用
收藏
页码：183 / 202
页数：20
相关论文
共 50 条
  • [31] Handling Refinement of Continuous Behaviors: A Proof Based Approach with Event-B
    Dupont, G.
    Ait-Ameur, Y.
    Pantel, M.
    Singh, N. K.
    2019 13TH INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING (TASE 2019), 2019, : 9 - 16
  • [32] Core Hybrid Event-B I: Single Hybrid Event-B machines
    Banach, Richard
    Butler, Michael
    Qin, Shengchao
    Verma, Nitika
    Zhu, Huibiao
    SCIENCE OF COMPUTER PROGRAMMING, 2015, 105 : 92 - 123
  • [33] Modelling Hybrid Systems in Event-B and Hybrid Event-B: A Comparison of Water Tanks
    Banach, Richard
    Butler, Michael
    FORMAL METHODS AND SOFTWARE ENGINEERING, ICFEM 2016, 2016, 10009 : 90 - 105
  • [34] Formally verified architectural patterns of hybrid systems using proof and refinement with Event-B
    Dupont, Guillaume
    Ait-Ameur, Yamine
    Singh, Neeraj Kumar
    Pantel, Marc
    SCIENCE OF COMPUTER PROGRAMMING, 2022, 216
  • [35] Formally Verified Architecture Patterns of Hybrid Systems Using Proof and Refinement with Event-B
    Dupont, Guillaume
    Ait-Ameur, Yamine
    Pantel, Marc
    Singh, Neeraj K.
    RIGOROUS STATE-BASED METHODS, ABZ 2020, 2020, 12071 : 169 - 185
  • [36] Core Hybrid Event-B II: Multiple cooperating Hybrid Event-B machines
    Banach, Richard
    Butler, Michael
    Qin, Shengchao
    Zhu, Huibiao
    SCIENCE OF COMPUTER PROGRAMMING, 2017, 139 : 1 - 35
  • [37] Enabling Analysis for Event-B
    Dobrikov, Ivaylo
    Leuschel, Michael
    ABSTRACT STATE MACHINES, ALLOY, B, TLA, VDM, AND Z (ABZ 2016), 2016, 9675 : 102 - 118
  • [38] A proposal for records in Event-B
    Evans, Neil
    Butler, Michael
    FM 2006: FORMAL METHODS, PROCEEDINGS, 2006, 4085 : 221 - 235
  • [39] Reasoned Modelling with Event-B
    Butler, Michael
    ENGINEERING TRUSTWORTHY SOFTWARE SYSTEMS (SETSS 2016), 2017, 10215 : 51 - 109
  • [40] A new Operators-Based Approach for the Event-B Refinement: QNoC Case Study
    Hariche, Abdelhamid
    Belarbi, Mostefa
    Daoud, Hayat
    2013 25TH INTERNATIONAL CONFERENCE ON MICROELECTRONICS (ICM), 2013,
12345