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 条
  • [1] A CSP account of Event-B refinement
    Schneider, Steve
    Treharne, Helen
    Wehrheim, Heike
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2011, (55): : 139 - 154
  • [2] The behavioural semantics of Event-B refinement
    Schneider, Steve
    Treharne, Helen
    Wehrheim, Heike
    FORMAL ASPECTS OF COMPUTING, 2014, 26 (02) : 251 - 280
  • [3] A Graphical Tool for Event Refinement Structures in Event-B
    Dghaym, Dana
    Trindade, Matheus Garay
    Butler, Michael
    Fathabadi, Asieh Salehi
    ABSTRACT STATE MACHINES, ALLOY, B, TLA, VDM, AND Z (ABZ 2016), 2016, 9675 : 269 - 274
  • [4] Managing LTL Properties in Event-B Refinement
    Schneider, Steve
    Treharne, Helen
    Wehrheim, Heike
    Williams, David M.
    INTEGRATED FORMAL METHODS, IFM 2014, 2014, 8739 : 221 - 237
  • [5] Refactoring Refinement Structure of Event-B Machines
    Kobayashi, Tsutomu
    Ishikawa, Fuyuki
    Honiden, Shinichi
    FM 2016: FORMAL METHODS, 2016, 9995 : 444 - 459
  • [6] Event-B Refinement for Continuous Behaviours Approximation
    Dupont, Guillaume
    Ait-Ameur, Yamine
    Pantel, Marc
    Singh, Neeraj K.
    AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, ATVA 2021, 2021, 12971 : 320 - 336
  • [7] On Information Flow Control in Event-B and Refinement
    Mu, Chunyan
    2013 INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING (TASE), 2013, : 225 - 232
  • [8] Language and tool support for event refinement structures in Event-B
    Fathabadi, Asieh Salehi
    Butler, Michael
    Rezazadeh, Abdolbaghi
    FORMAL ASPECTS OF COMPUTING, 2015, 27 (03) : 499 - 523
  • [9] Automatic refinement for Event-B through annotated patterns
    Siala, Badr
    Bodeveix, Jean-Paul
    Filali, Mamoun
    Bhiri, Mohamed Tahar
    2017 25TH EUROMICRO INTERNATIONAL CONFERENCE ON PARALLEL, DISTRIBUTED AND NETWORK-BASED PROCESSING (PDP 2017), 2017, : 287 - 290
  • [10] Extracting Traceability between Predicates in Event-B Refinement
    Saruwatari, Shinnosuke
    Ishikawa, Fuyuki
    Kobayashi, Tsutomu
    Honiden, Shinichi
    2017 24TH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE (APSEC 2017), 2017, : 61 - 70
12345