文档介绍：湖南大学
硕士学位论文
面向自动化模型检测的模型提取工具的设计与实现
姓名:王大伟
申请学位级别:硕士
专业:计算机科学与技术
指导教师:张大方
20090521
摘要随着计算机软件日益复杂,如何保证其正确性和可靠性成为十分紧迫的问题。模型检测是一种验证有限状态系统的时序逻辑属性的形式化方法,已经在硬件电错误等,因此从源代码中直接提取验证模型存在强烈的实际需求。.贝尔实验室开发的是优秀的模型检测工具,其建模语言是鳦语言是应用部分语言特性,特别是几种复杂的结构,比如递归函数、枚举类型和指针等。并语言编写的应用程序中的多种错误,比如死锁等性质。作者使用进行了路、驱动程序和安全协议等领域获得了巨大的成功。应用模型检测技术到高级程序设计语言实现的系统的难点是提取抽象模型,通常的办法是手工构造。然而这个方法存在一些不足,如成本过高,易引入建模最广泛的程序设计语言之一,,〉姆椒ǎ虾玫卮砹薈的大开发了一个模型提取工具。从功能上来说,分为前端和后端。前端是一个分析器,具有对创虢写史ǚ治龊陀锓ǚ治龅墓δ堋:蠖嗽蚴且个转换器,实现了从氲絇代码的系统转换。而且,为了减小模型的规模,加快模型提取的速度或者提高模型的执行效率,中使用了一些简单的抽象机制和优化技术。显著降低了建模的开销。结合,能够自动地检测使用一定数量的测试。在实验中,依靠生成的模型,,以及对两个经典互斥算法的实现中的活锁错误。因此我们认为在检测—绦蚍矫婢哂幸欢ǖ氖涤眉壑怠关键词:形式化方法;模型检测;模型提取;.籗籔硕貉宦畚
.,瑆,..琩琲,.,,琒,.瓵甧猠瑂甋,.·.
篎;籑硕学位论文;—籗
一一一一鼍事鼍皇曼曼鼍鼍皇暑詈皇鼍皇鼍暑竞令夯适铑夯驶事决荆曼绢忽荆插图索引难橹す獭深度优先搜索算法⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯有限状态自动机和⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯..和的扩展异步积⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯应用偏序归约技术的效果⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.的基本结构⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯分析器幕玖鞒獭分析器的记号表片段⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯根结点⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.基本变量符号表⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯结构体符号表⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯疟怼扑鉧的搿提取模型的过程⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯..扑鉧的搿发现语法错误⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯..的模拟执行⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯的验证执行⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯械慕獭械难酚锞洹械奶S锞洹械乃啤变量作用域管理机制⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.不~致的枚举类型模型⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.的类图切片⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.函数定义结点⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯的命令行界面⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯..械膖.⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯..械难≡裼锞洹刚肽P汀图图图图图图图图图图图图图图图图图图图图图图图图图图图图图图图图腁⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯面向自动化模型柃测的模型提取丁只的设汁’迪.
镜膚语句模型⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯提取的循环模型⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯鼳调用墓叵低肌卸霞浣拥莨楹乃惴ā哪诹DP汀耐酵ㄐ拍P汀莨楹P汀P陀呕算法伪代码⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯算法伪代码⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯..算法的活锁错误示意图⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯算法的活锁错误原因⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.算法的活锁错误示意图⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯算法的活锁错误原因⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.囊桓鯾⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯镜膇锞淠P汀鼳,珻互相调用关系图⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯..囊觳酵ㄐ拍P汀图图图图图图图图图图图图图图图图图图硕』孤畚
⋯一—————————猲——黫曼个决韭曼詈曼曼鼍皇崖附表索引事件发生事件关联其它情况幕臼堇嘈汀的基本类型映射表⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯算法的死锁检测结果⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯算法的死锁检测结果⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯算法的活锁检测结果⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯算法的活锁检测结果⋯⋯⋯