基于Rebeca模型的硬件设计形式化验证

• 作者: 刘晓芹 吕晓明 连光耀 黄考利
• 来源期刊: 计算机测量与控制
• 关键词: 形式化验证 Rebeca模型 Modere
• 年，卷（期）: 2009,（5）
• 所属期刊栏目: 试验与验证技术
• 页码范围: 914-916
• 页数: 3页
• 分类号: TP206.1
• 语种: 中文

摘要

形式化验证是对传统验证方法的补充,是数字电路验证的一条有效途径,对于并发系统,行为建模是一种非常合适的建模方法;Rebeea是由Sirjani和Movaghar提出的一种基于行为的建模语言,支持形式化,一方面,Rebeca是一种类Java的语言,软件工程师很容易使用,另一方面,它是一种支持形式化验证及其相关理论的模型语言.可以为不精通干形式化方法的开发人员和研究人员提供方便的验证过程;在深入研究Rebeea的基础上,采用Rebeea对硬件设计进行建模,然后Modere形式化验证工具对AIES密码芯片进行形式化验证.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	黄考利		62	484	13.0	18.0
2	刘晓芹		18	118	7.0	10.0
6	连光耀		55	411	12.0	17.0
7	吕晓明		19	138	8.0	11.0