基于事件B的处理器形式化建模方法的研究

• 作者: 余洁 周学海 李曦 高妍妍
• 来源期刊: 系统仿真学报
• 学科: 工学
• 关键词: 事件B 抽象系统 资源 指令 控制
• 年，卷（期）: 2007,（3）
• 所属期刊栏目: 仿真计算机与仿真软件及仿真实验环境
• 页码范围: 543-548
• 页数: 6页
• 分类号: TP301
• 字数: 5486字
• 语种: 中文
• DOI: 10.3969/j.issn.1004-731X.2007.03.020

摘要

针对当前可重定向的模拟器生成平台的需求和现有的处理器模型的缺陷,提出了一种基于事件B的处理器模型EBPM(Event B based Processor Model).利用事件B中的抽象系统,通过资源、指令和控制三个子模型从结构、行为和时序三方面对处理器进行建模,每个子模型中分别由抽象系统的状态和事件两部分刻画其静态行为和动态行为.该模型不但具有很强的灵活性和扩展性,还支持指令级和周期级两个层次的建模.通过对MIPS处理器的流水线进行形式化建模的实例说明了EBPM的有效性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李曦	中国科学技术大学计算机科学技术系	119	751	13.0	21.0
2	周学海	中国科学技术大学计算机科学技术系	109	885	17.0	24.0
3	高妍妍	中国科学技术大学计算机科学技术系	11	24	3.0	4.0
4	余洁	中国科学技术大学计算机科学技术系	8	33	3.0	5.0