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