基于uppaal平台的ahb总线形式化验证方法研究

《基于uppaal平台的ahb总线形式化验证方法研究》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、学校代码１０６０８学号２０１３０８１２０３４０２分类号ＴＰ３０１．１密级公开ＧｕａｎｘｉＵｎｉｖｅｒｓｉｔｆｏｒＮａｔｉｏｎａｌｉｔｉｅｓｇｙ硕壬学位备文基于ＵＰＰＭＬ平台的ＡＨＢ总线形式化验证方法研巧硏究生姓名；吴丽佳导师姓名职務、教巧：吴尽昭学科专业：计算化应用技术所属学院：信息科学与工程学院年级：２０１３级论文完成时间：２０１６年４月？论文独创性声明人巧导师的指导下，独立撰学位论文，是本本人郑垂声明：所提交的引用的内容外，木

2、论义不含其他个人诚巧他机的亢成的。除文中己经巧剛果、妙袭等违反学术道德规范构己经发表或撰巧过的硏究成，化没有飄窃和集佈，均＾在丈中則口的巧权巧为＝对本义的硏究做出軍耍巧献的个人由本声明而引起的法律贵巧。确方式标明。本人應轟承巧月／。鬥！１年：期如巧巧生豁名爾隹ｆ（ｌ＾羣论文使用搔权声明留。学校有本人完全了解广西巧族大学有关保、使用学位论文的规定权保留并向閨家巧关部ｎ或机构送交学位论文的复印件和电子文巧，可从位论文。除在保密期内的保、汇编学采用影印、缩印或其他复制手段保存

3、＾包括刊登）论文的全密论文外阅，可从公化，允许学位论文被查阅和借。部或部分内容、曰期：年６＂ｎ研究生签名：果啼乳签。年Ｈ导师名：＾基于UPPAAL平台的AHB总线形式化验证方法研究摘要AMBA总线规范是ARM公司设计的一种用于高性能嵌入式系统的总线标准。AHB总线是高性能系统总线，它能够维持外部内存带宽并且可以为CPU连接、片上内存和其他直接内存访问（DMA）设备间的通信提供接口。系统中微小的逻辑错误都能导致严重的后果，研究并验证嵌入式系统AHB总线技术规范是保障系统安全、快速、高

4、效地运行的重要组成部分。验证面临的问题是如何保证在对实时系统一致性建模的前提下对模型做具有完备性验证，本文采用了形式化的模型验证技术。本文首先介绍了AMBAAHB的相关内容，包括AHB总线结构和基于SystemC语言的AHB事务级描述；而后提出了SystemC语言的UPPAAL时间自动机语义；并根据之前所得到的AHB的SystemC描述，提出了AHB事务级描述到时间自动机模型的转换方法，最后建立了一种利用UPPAAL工具的AHB验证方案，并给出了部分验证实例。根据本文研究进展所示，基于UPPAAL平台的时间

5、自动机验证方案，可以有效的验证AHB总线的各个性能属性，为AHB的几个重要性质验证问题提供了一种较好的解决办法。关键词：AHB总线UPPAAL模型检测形式化验证IRESEARCHONAHBBUSFORMALVERIFICATIONMETHODBASEDONUPPAALABSTRACTAMBABusisoneoftheBUSstandardthatisusedforhighperformanceembeddedsystemofARM.AHBisahighperformancesystembus.ItIsabl

6、etokeeptheexternalmemorybandwidthandprovidesinterfacescommunicatingwithCPU，memoryon-chipandotherDMA.Itiswell-knownthatatinydefectmightmakeasystemfail,soitisnecessaryandvaluabletoverifyaAHBimplementationbeforeitisonthemarket.However,thechallengeofverificati

7、onishowtoensurethecorrectnessofrealsystem,inthispaper,weadoptoneofthemostpopularformalmethods,e.g.,modelchecking.Inthispaper,weefirstintroducethearchitectureandSystemCbasedtransactionmodelofAMBAAHB;andthentheUPPAALstyledtimedautomatonsemanticsoftheSystemCl

8、anguage;Then，withtransactionmodelofAHBandtheprevioussemantics,awayoftranslationAMBAAHBintotimedautomataisshown;Andfinally,weintroduceourverificationprocedureswithUPPAALbyseveralconcreteexamples.Accordingtothe