硬件系统SystemC～（FL）设计模型的SPIN验证

发布时间：2020-06-11 21:11

【摘要】：随着系统设计复杂度的提高,设计验证已成为系统设计的瓶颈;传统验证技术已不能满足需要,形式化验证技术是适应这种需求而产生的新技术。形式化验证方法包括算法验证、属性验证和等价性验证等方法。论文的研究领域为属性验证。属性验证又包括定理证明、语言包含、符号模型检测等方法。常见的符号模型检测器有CTL模型检测器如SMV验证工具;LTL模型检测器如SPIN验证工具。 SPIN这一软件验证工具,是于1989年由贝尔实验室J.Holzmann等开发的模型检测器。主要面向分布式软件和协议系统的验证。SPIN使用PROMELA作为验证的模型语言,并使用线性时态逻辑(LTL)公式描述属性,应用自动机理论实现系统的模拟运行和正确性验证。 SPIN对系统的验证过程是首先用PROMELA语言建立系统的状态机模型,然后抽象出用LTL公式表示的系统需求属性的形式化描述,系统的正确性需求属性也可以在PROMELA中通过特殊标记来描述。验证的目标是判断系统模型与其抽象属性是否相符。 SystemC~(FL)是基于进程代数ACP的SystemC语言的形式化语言。既表示了SystemC模型的语义,又是对SystemC模型中进程的行为分析。SystemC~(FL)的目的是对SystemC设计的形式化描述以及SystemC进程的形式化行为分析。SystemC~(FL)可对各种各样的系统建模(有限状态系统、实时系统等)。 为验证SystemC~(FL)建模的并行及硬件系统,选择SPIN模型检测器作为验证工具。论文中通过将硬件系统的SystemC~(FL)模型转换成PROMELA模型,然后用SPIN验证工具对模型进行验证。通过论文中研究的验证方法,可以在一定程度上实现应用SPIN模型检测器对硬件系统设计的验证。
【图文】：

太大我们则通常采用bit一hahsnig验证模式进行属性验证。然后对验证结果进行分析，找出模型中的错误，进行修改后重新验证，，直到P中的每个属性进行一一验证后，系统的验证才结束。如图2一9表示SPNI的验证过程图示。图2一9:SPNI的验证过程
【学位授予单位】：兰州大学
【学位级别】：硕士
【学位授予年份】：2006
【分类号】：TP368.1

【相似文献】

相关期刊论文 前10条

1 刘晓芹;黄考利;连光耀;吕晓明;;基于Rebeca模型的硬件设计形式化验证[J];计算机测量与控制;2009年05期

2 杨红丽,王曙燕,韩俊刚;基于形式化的面向对象开发方法(FMOO)[J];计算机应用;2000年05期

3 周宏斌,黄连生,桑田;基于串空间的安全协议形式化验证模型及算法[J];计算机研究与发展;2003年02期

4 陈江;陈建国;陆慧娟;王康健;;UML时间顺序图的实时系统建模及验证[J];中国计量学院学报;2010年01期

5 侯峻峰,张磊,黄连生;一种新的安全协议形式化验证方法[J];计算机研究与发展;2004年08期

6 郭建;时序电路的形式化证明[J];现代电子技术;2005年20期

7 王金双;杨华兵;张兴元;王元元;张毓森;;电梯控制系统在Isabelle/HOL中的活动性证明[J];计算机工程与应用;2008年27期

8 潘国华;王惠芳;;密码API安全性分析[J];计算机安全;2009年06期

9 郭建,韩俊刚;SOC的形式化验证方法[J];西安邮电学院学报;2005年03期

10 张海宾;段振华;;混合投影时序逻辑与混合系统的形式化验证[J];计算机科学;2007年11期

相关会议论文 前10条

1 苗洁君;王克;;密码模块的形式化设计和验证研究[A];第二十一次全国计算机安全学术交流会论文集[C];2006年

2 吴铃铃;周干民;何伟;高明伦;;IP软核的形式化验证[A];全国第十五届计算机科学与技术应用学术会议论文集[C];2003年

3 刘力轲;游定山;杨佳;元国军;沈华;;集合通信芯片物理设计阶段的验证方法[A];第十五届计算机工程与工艺年会暨第一届微处理器技术论坛论文集（A辑）[C];2011年

4 郭建;韩俊刚;;基于PSL的FIFO的验证[A];第五届中国测试学术会议论文集[C];2008年

5 余兴超;马争先;王玉斌;董荣胜;;基于UPPAAL的简单网络支付协议形式化验证[A];广西计算机学会2010年学术年会论文集[C];2010年

6 李彩虹;章超;李廉;孙守卿;;分布式同步仲裁器电路的SPIN建模和验证[A];2005年全国理论计算机科学学术年会论文集[C];2005年

7 何青;骆翔宇;苏开乐;;对弈必胜策略的符号化模型检测[A];2006年全国理论计算机科学学术年会论文集[C];2006年

8 薛慧琦;吴恒;;由程序规约推导程序[A];2005年全国理论计算机科学学术年会论文集[C];2005年

9 郭华;庄雷;;电子商务协议的形式化验证方法及FR验证实例[A];2005年全国理论计算机科学学术年会论文集[C];2005年

10 陈博文;郭琦;沈海华;;浮点乘加部件的自动化形式验证[A];第六届中国测试学术会议论文集[C];2010年

相关博士学位论文 前10条

1 张海宾;混合系统的形式化验证[D];西安电子科技大学;2007年

2 许可;网格服务流的状态π演算形式化验证技术研究与应用[D];清华大学;2007年

3 沈胜宇;模型检验的反例解释[D];国防科学技术大学;2005年

4 张鹏飞;Agent通信的全信息形式语用方法[D];北京邮电大学;2007年

5 李梦君;安全协议形式化验证技术的研究与实现[D];国防科学技术大学;2005年

6 范年柏;程序正确性验证的几个问题[D];湖南大学;2005年

7 张秀国;基于过程网络的服务协同计算模型研究[D];大连海事大学;2006年

8 岳华伟;对一种SOC总线系统的验证[D];中国科学技术大学;2007年

9 程亮;基于模型检测的安全操作系统验证方法研究[D];中国科学技术大学;2009年

10 王小兵;面向对象MSVL语言及其在组合Web服务验证中的应用[D];西安电子科技大学;2009年

相关硕士学位论文 前10条

1 李彩虹;硬件系统SystemC～（FL）设计模型的SPIN验证[D];兰州大学;2006年

2 吴孝军;基于SPIN的ATM交换机行为的验证[D];兰州大学;2006年

3 林立;基于高阶逻辑系统HOL的数字硬件形式化验证[D];西安电子科技大学;2005年

4 闫硕;基于多项式符号代数的电路形式验证[D];北京交通大学;2011年

5 王莉;供热混合系统的抽象及其形式化验证[D];华中科技大学;2004年

6 马小龙;形式化验证在Office安全中的应用研究[D];中国人民解放军信息工程大学;2005年

7 杨汉明;基于CPS的实时系统的面向方面的形式化验证方法[D];广东工业大学;2011年

8 郑强;基于SPIN的802.1X协议形式化验证和改进[D];华东理工大学;2012年

9 廖军和;深亚微米EoPDH专用集成电路的设计与实现[D];合肥工业大学;2009年

10 姜玉蓉;LINUX内核进程间通信的模型检测研究[D];湖南大学;2009年

本文编号：2708462