-
题名基于Rebeca模型的硬件设计形式化验证
- 1
-
-
作者
刘晓芹
黄考利
连光耀
吕晓明
-
机构
军械工程学院
陆军航空兵学院
-
出处
《计算机测量与控制》
CSCD
北大核心
2009年第5期914-916,共3页
-
基金
总装备部基金资助项目(60771063)
-
文摘
形式化验证是对传统验证方法的补充,是数字电路验证的一条有效途径,对于并发系统,行为建模是一种非常合适的建模方法;Rebeca是由Sirjani和Movaghar提出的一种基于行为的建模语言,支持形式化,一方面,Rebeca是一种类Java的语言,软件工程师很容易使用,另一方面,它是一种支持形式化验证及其相关理论的模型语言,可以为不精通于形式化方法的开发人员和研究人员提供方便的验证过程;在深入研究Rebeca的基础上,采用Rebeca对硬件设计进行建模,然后Modere形式化验证工具对AES密码芯片进行形式化验证。
-
关键词
形式化验证
rebeca模型
modere
-
Keywords
formal verification: rebeca model: modere
-
分类号
TP206.1
[自动化与计算机技术—检测技术与自动化装置]
-