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

摘要：

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

关键词：形式化验证、Rebeca模型、Modere

所属期刊栏目：17

分类号：TP206.1(自动化技术及设备)

资助基金：总装备部基金资助项目60771063

在线出版日期：2009-06-26（万方平台首次上网日期，不代表论文的发表时间）

页数：共3页

页码：914-916