资源描述：
《支持协商的网构软件体系结构行为建模与验证new》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。
1、ISSN1000-9825,CODENRUXUEWE-mail:jos@iscas.ac.cnJournalofSoftware,Vol.19,No.5,May2008,pp.1099−1112http://www.jos.org.cnDOI:10.3724/SP.J.1001.2008.01099Tel/Fax:+86-10-62562563©2008byJournalofSoftware.Allrightsreserved.∗支持协商的网构软件体系结构行为建模与验证1,21,21,2+1,2
2、1,2周立,陈湘萍,黄罡,孙艳春,梅宏1(北京大学信息科学技术学院软件研究所,北京100871)2(北京大学高可信软件技术教育部重点实验室,北京100871)Negotiation-EnabledModelingandVerificationofArchitecturalBehaviorofInternetware1,21,21,2+1,21,2ZHOULi,CHENXiang-Ping,HUANGGang,SUNYan-Chun,MEIHong1(SoftwareInstitute,Schoo
3、lofElectronicsEngineeringandComputerScience,PekingUniversity,Beijing100871,China)2(KeyLaboratoryofHighConfidenceSoftwareTechnologiesofMinistryofEducation,PekingUniversity,Beijing100871,China)+Correspondingauthor:E-mail:huanggang@sei.pku.edu.cn,http:/
4、/www.sei.pku.edu.cnZhouL,ChenXP,HuangG,SunYC,MeiH.Negotiation-EnabledmodelingandverificationofarchitecturalbehaviorofInternetware.JournalofSoftware,2008,19(5):1099−1112.http://www.jos.org.cn/1000-9825/19/1099.htmAbstract:Fortheuncertaintyandincomplet
5、enessinthebehaviorofInternetware,anegotiation-enabledapproachtomodelingandverificationofsoftwarearchitecturalbehaviorisproposedinthispaper.Inthemodeling,thisapproachtakesthenotationsofUMLsequencediagramandextendthemodelwithnewelementstosupporttheunce
6、rtaintyandincompleteness.Intheverification,themodelcheckerSpinisemployedforcheckingbehaviormodels.Inaddition,anegotiation-enabledsolutionisproposedfortheverificationwithuncertainandincompletemodelbasedonthecounterexampleguidedabstractrefinementmethod
7、.Keywords:Internetware;softwarearchitecture;modelchecking;behaviormodel摘要:针对网构软件行为中的不确定性和不完整性,提出了一种支持协商的网构软件体系结构行为建模与验证方法.在建模中,该方法借鉴了UML时序图元素表示法,并增加了建模元素支持行为的不确定与不完整建模.在验证中,除了集成广泛应用的模型检查工具Spin以提供行为模型的验证能力以外,还引入了基于反例引导的抽象-精化过程思想的协商检查,以解决不确定和不完整建模所带来的正
8、确性验证问题.关键词:网构软件;软件体系结构;模型检查;行为模型中图法分类号:TP311文献标识码:A软件体系结构(softwarearchitecture,简称SA)中的行为建模,本身就具有不确定性和不完整性的特点.不确定性指的是系统的部分行为是无法精确描述的.造成不确定的因素,有可能是设计人员缺乏对系统细节的足够了解而无法给出精确的信息,也可能是系统中一些无法预计的行为造成的.不完整性指的是其行为描述可能只包括部分行为或者对验证所需信息不够充足.而体系结构的设计往往是针对大型系统的,描述其完
