基于Mealy机精化关系的验证算法
文献类型：期刊论文
| 作者 | 梁虹 ; 金乃咏 |
| 刊名 | 计算机应用与软件
 |
| 出版日期 | 2012 |
| 卷号 | 29期号:8页码:169-172 |
| 关键词 | 形式验证 性质验证 精化 Mealy机 |
| ISSN号 | 1000-386X |
| 其他题名 | a verification method based on refinement of mealy machine |
| 中文摘要 | 与传统验证方法相比,形式验证技术因其完备性,已在数字电路设计领域中得到越来越多的关注。通过对形式验证技术和状态机的研究,在LTL公式的可实现策略基础上,提出一个基于Mealy机精化关系的验证算法,实现了一个搜索工具原型:支持算术表达式的LTL性质描述,在设计空间中搜索满足给定规范的输入输出信号。该技术可应用于定位电路设计中满足给定功能性质的代码片段。 |
| 英文摘要 | Compared with traditional verification methods,formal verification,as one of the complementary approaches,has received more and more attention in digital circuit design field.So through the study of formal verification and the state machines,a verification method based on the refinement of Mealy machine has been proposed according to achievable policy of LTL formula.And we have implemented a prototype of search tool: it supports the arithmetic expressions in LTL property description and finds out in design space the given input/output signals satisfying the specification.This enabling technology is able to be applied to the design of locating circuit to satisfy the code segment with certain behavioural properties. |
| 学科主题 | Computer Science (provided by Thomson Reuters) |
| 收录类别 | CNKI ; CSCD ; WANFANG |
| 资助信息 | 国家自然科学基金项目(60970030)|教育部留学回国人员科研启动基金项目(外教司[2006J331])资助 |
| 语种 | 中文 |
| CSCD记录号 | CSCD:4603473 |
| 公开日期 | 2013-09-17 |
| 源URL | [http://ir.iscas.ac.cn/handle/311060/15001]  |
| 专题 | 软件研究所_软件所图书馆_期刊论文 |
| 推荐引用方式 GB/T 7714 | 梁虹,金乃咏. 基于Mealy机精化关系的验证算法[J]. 计算机应用与软件,2012,29(8):169-172. |
| APA | 梁虹,&金乃咏.(2012).基于Mealy机精化关系的验证算法.计算机应用与软件,29(8),169-172. |
| MLA | 梁虹,et al."基于Mealy机精化关系的验证算法".计算机应用与软件 29.8(2012):169-172. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。