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 条
  • [21] Foundations for using linear temporal logic in Event-B refinement
    Thai Son Hoang
    Schneider, Steve
    Treharne, Helen
    Williams, David M.
    FORMAL ASPECTS OF COMPUTING, 2016, 28 (06) : 909 - 935
  • [22] Refinement and Validation of the Immune System Based on the Event-B Method
    Zou, Sheng-rong
    Chen, Li
    Wang, Chen
    Shu, Yu-dan
    2019 4TH INTERNATIONAL CONFERENCE ON COMPUTATIONAL INTELLIGENCE AND APPLICATIONS (ICCIA 2019), 2019, : 16 - 20
  • [23] Understanding and Planning Event-B Refinement through Primitive Rationales
    Kobayashi, Tsutomu
    Ishikawa, Fuyuki
    Honiden, Shinichi
    ABSTRACT STATE MACHINES, ALLOY, B, TLA, VDM, AND Z, ABZ 2014, 2014, 8477 : 277 - 283
  • [24] Developing mode-rich satellite software by refinement in Event-B
    Iliasov, Alexei
    Troubitsyna, Elena
    Laibinis, Linas
    Romanovsky, Alexander
    Varpaaniemi, Kimmo
    Ilic, Dubravka
    Latvala, Timo
    SCIENCE OF COMPUTER PROGRAMMING, 2013, 78 (07) : 884 - 905
  • [25] Consistency-preserving refactoring of refinement structures in Event-B models
    Kobayashi, Tsutomu
    Ishikawa, Fuyuki
    Honiden, Shinichi
    FORMAL ASPECTS OF COMPUTING, 2019, 31 (03) : 287 - 320
  • [26] An Automatic Refinement for Event-B Through Annotated Temporal Logic Patterns
    Siala, Badr
    Bhiri, Mohamed T.
    COMPUTATIONAL COLLECTIVE INTELLIGENCE, ICCCI 2022, 2022, 13501 : 624 - 637
  • [27] A refinement development approach for enhancing the safety of PLC programs with Event-B
    Mao, Xia
    Zhang, Yueling
    Shi, Jianqi
    Huang, Yanhong
    Li, Qin
    SCIENCE OF COMPUTER PROGRAMMING, 2022, 215
  • [28] Trustworthy smart city systems using refinement and Event-B Theories
    Alkhammash, Eman H.
    MULTIMEDIA TOOLS AND APPLICATIONS, 2022, 81 (01) : 615 - 636
  • [29] Extending SYSML with Refinement and Decomposition Mechanisms to Generate EVENT-B Specifications
    Bougacha, Racem
    Laleau, Regine
    Collart-Dutilleul, Simon
    Ben Ayed, Rahma
    THEORETICAL ASPECTS OF SOFTWARE ENGINEERING, TASE 2022, 2022, 13299 : 256 - 273
  • [30] Trustworthy smart city systems using refinement and Event-B Theories
    Eman H. Alkhammash
    Multimedia Tools and Applications, 2022, 81 : 615 - 636
12345