| 基于事件B的处理器形式化建模方法的研究 |
| |
| 引用本文： | 余洁,李曦,周学海,高妍妍.基于事件B的处理器形式化建模方法的研究[J].系统仿真学报,2007,19(3):543-548. |
| |
| 作者姓名： | 余洁 李曦 周学海 高妍妍 |
| |
| 作者单位： | 中国科学技术大学计算机科学技术系,安徽合肥,230027 |
| |
| 基金项目： | 国家自然科学基金;高等学校博士学科点专项科研项目 |
| |
| 摘 要： | 针对当前可重定向的模拟器生成平台的需求和现有的处理器模型的缺陷,提出了一种基于事件B的处理器模型EBPM(EventBbasedProcessorModel)。利用事件B中的抽象系统,通过资源、指令和控制三个子模型从结构、行为和时序三方面对处理器进行建模,每个子模型中分别由抽象系统的状态和事件两部分刻画其静态行为和动态行为。该模型不但具有很强的灵活性和扩展性,还支持指令级和周期级两个层次的建模。通过对MIPS处理器的流水线进行形式化建模的实例说明了EBPM的有效性。
|
| 关 键 词： | 事件B 抽象系统 资源 指令 控制 |
| 文章编号： | 1004-731X（2007）03-0543-06 |
| 收稿时间： | 2005-11-14 |
| 修稿时间： | 2006-04-13 |
Research on Formal Modeling for Processor Based on Event B |
| |
| YU Jie,LI Xi,ZHOU Xue-hai,GAO Yan-yan.Research on Formal Modeling for Processor Based on Event B[J].Journal of System Simulation,2007,19(3):543-548. |
| |
| Authors: | YU Jie LI Xi ZHOU Xue-hai GAO Yan-yan |
| |
| Institution: | Department of Computer Science, University of Science and Technology of China, Hefei 230027, China |
| |
| Abstract: | |
| |
| Keywords: | event B abstract system resource instruction control |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
