ISSN1009-3044E-mail:xsjl@cccc.net.cn电脑知识与技术第卷第期年月ComputerKnowledgeandTechnology电脑知识与技术611http://www(2010.dnzs.net.cn4)Vol.6,No.11,April2010,pp.2624-2626Tel:+86-551-56909635690964基于SPIN内核的SDL模型检验工具设计黄山1，3，黄忠见2，韩柯3，王建伟3（1.中国人民解放军理工大学指挥自动化学院，江苏南京210007；2.西昌卫星发射中心指挥控制中心，四川西昌610005；3.中国电子系统设备工程公司研究所，北京100141）摘要：规格描述语言SDL目前广泛应用于复杂通信协议和软件系统的建模。使用模型检验技术对SDL进行分析和验证可以检测出模型中的逻辑错误，大大提高SDL建模结果的精确性。论文研究了SDL的形式化语义SDL/PR中常用部分与模型检验工具SPIN的输入语言Promela之间的语义映射规则，并以此为基础开发了一个基于SPIN内核的SDL模型检验器SSMCTool。关键词：SDL；ModelChecking；语义转换；SPIN；模型验证中图分类号：TP311文献标识码：A文章编号：1009-3044(2010)11-2624-03CheckingToolDesignofSDLModelBasedonSPINKernelHUANGShan1,3,HUANGZhong-jian2,HANKe3,WANGJian-wei3(1.InstituteofCommandandControl,PLAUniversityofScienceandTechnology,Nanjing210007,China;2.TheMissionCommandandControlCenter,XichangSatelliteLaunchCenter,Xichang615000,China;3.InstituteofChinaElectronicSystemsEquipmentCompany,Beijing100141,China)Abstract:SDL（SpecificationandDescriptionLanguage）iswidelyappliedinthemodelingofcomplexcommunicationprotocolandsoft-ware.ModelcheckingcanfindoutSDL'slogicfaultandgreatlyimproveitsaccuracy.ThepaperhasstudiedthemappingrulebetweenSDL/PRandPromela,whichistheinputlanguageofthemodelcheckerSPIN,andthenprogrammedaSDLmodelcheckerSSMCToolthatisbasedonSPINkernel.Keywords:SDL;ModelChecking;semantictransition;SPIN;modelverification规格描述语言SDL（SpecificationandDescriptionLanguage）[1]是ITU定义的一种数据类型支持能力极强的形式化描述语言，其核心基于扩展有限状态机的通信进程模型。SDL目前大量应用于电信领域中的通信协议建模以及描述具备活性离散系统特征的软件。模型检验（ModelChecking）[2-3]是一种针对有限状态系统的形式化自动验证技术，自提出至今已被应用于计算机硬件、通信协议、安全认证协议等方面的分析与验证中，取得了令人瞩目的成绩。使用模型检验技术对SDL模型进行分析与验证，可以减少模型中的设计错误，提高建模的精确性[4]。对于SDL模型来说，如果对其直接模型检验，则需要重新构建专用的模型检验工具，这是一项十分烦琐和困难的工作。将其转换为某种模型检验工具的形式化输入，则可以免去重新构建模型检验工具所需要的额外精力。出于以上因素考虑，本文研究了SDL模型的形式化文法SDL/PR[4]向模型检验工具SPIN的输入语言Promela[2]的语义转换规则，构造了文法翻译器SDL2PromelaTranslator.exe，并设计实现了一个基于SPIN内核的SDL模型检验工具SSMCTool。1文法翻译器SDL2Promela的构造1.1SDL/PR到Promela的语义转换规则首先要实现系统结构的转换。SDL的模型结构是形如System-Block-Process的层次性结构，而Promela中构建系统基本行为的单元是进程(pro