面向自动化模型检测模型提取工具设计和实现

《面向自动化模型检测模型提取工具设计和实现》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、硕l：学位论文摘要随着计算机软件日益复杂，如何保证其正确性和可靠性成为十分紧迫的问题。模型检测是一种验证有限状态系统的时序逻辑属性的形式化方法，已经在硬件电路、驱动程序和安全协议等领域获得了巨大的成功。应用模型检测技术到高级程序设计语言实现的系统的难点是提取抽象模型，通常的办法是手工构造。然而这个方法存在一些不足，如成本过高，易引入建模错误等，因此从源代码中直接提取验证模型存在强烈的实际需求。．贝尔实验室开发的SPIN是优秀的模型检测工具，其建模语言是PROMELA，而C语言是应用最广泛的程序设计语言之

2、一，因此本文的主要研究内容定位于ANSI．C程序的模型提取技术，从而达到使用SPIN自动化模型检测C程序的目的。本文设计了一套对ANSI．C程序进行模型提取的方法，较好地处理了C的大部分语言特性，特别是几种复杂的结构，比如递归函数、枚举类型和指针等。并开发了一个模型提取工具C2Spin。从功能上来说，C2Spin分为前端和后端。前端是一个分析器，具有对C源代码进行词法分析和语法分析的功能。后端则是一个转换器，实现了从C代码到PROMELA代码的系统转换。而且，为了减小模型的规模，加快模型提取的速度或者提

3、高模型的执行效率，C2Spin中使用了一些简单的抽象机制和优化技术。C2Spin显著降低了建模的开销。结合C2Spin，SPIN能够自动地检测使用C语言编写的应用程序中的多种错误，比如死锁等性质。作者使用C2Spin进行了一定数量的测试。在实验中，依靠C2Spin生成的模型，我们发现了SPIN4．3．0的一个语义错误，以及Holzmann对两个经典互斥算法的实现中的活锁错误。因此我们认为C2Spin在检测ANSI—C程序方面具有一定的实用价值。关键词：形式化方法；模型检测；模型提取；ANSI．C；SPI

4、N；PROMELAIIAbstractWiththeincreasingcomplexityofcomputersoftwares，itisnecessaryandurgenttoensurethecorrectnessandreliabilityofthesesystems．ModelCheckingisaformalmethodforverifyingthetemporallogicpropertiesoffinitestatesystems，andhasgottenhugesuccessinare

5、assuchashardwarecircuits，devicedriversandsecurityprotocols．Thedifficultyofapplyingmodelcheckingtechniquetothesystemsimplementedinhigh．1evelprogramminglanguageisextractinganabstractmodelwhichisusuallydonebyhand．Butthisapproachhassomeweaknesses，forinstance

6、，thecostofmodelingisfairlyhighandtheartificialmodelsareerror。prone，thereforetherearestrongpracticalrequirementsforextractingverificationmodelfromthesourcecodedirectly．SPINisoneofthemostexcellentmodelcheckerswhosemodelinglanguageisPROMELA，whiletheCprogram

7、minglanguageisoneofthemostpopularlanguages，SOthemaincontentofthethesisfocusesonthetechniqueofmodelextractionforCprogramsinordertoachievethegoalofmodelcheckingCprogramswithSPINautomatically．Inthisthesis，wedesignasetofmethodsforextractingverificationmodels

8、fromtheANSI．CprogramswhichhandlemostlanguagefeaturesinCproperly,especiallyafewtoughstructures，suchasrecursivefunction，enumerationtypeandpointer．AndthenwedevelopamodelextractornamedC2Spin．C2Spinisdividedintotwopartsintemsof