基于时序描述逻辑的UML顺序图形式化方法.pdf

《基于时序描述逻辑的UML顺序图形式化方法.pdf》由会员上传分享，免费在线阅读，更多相关内容在应用文档-天天文库。

1、第39卷第3期计算机工程2013年3月V0l_39No．3ComputerEngineeringMarch2013·软件技术与数据库·文章编号：1000—_3428(2013)03—03一_05文献标识码。A中图分类号：TP182基于时序描述逻辑的UML顺序图形式化方法陈振庆(贺州学院计算机科学与工程系，广西贺州542800)摘要：根据统一建模语言(uML)顺序图的时序特征，提出一种基于时序描述逻辑ALCQIus的UML顺序图形式化方法。研究ALCQIus时序扩展部分的语法和语义、ALCQIus断言公式集一致性定理，给出ALCQIus断言公式集一致性推理

2、算法，并证明该推理算法的可判定性。以公安报警系统为例，说明基于ALCQIus的UML顺序图形式化规约和形式化验证具备可行性，并且ALCQIus为UML顺序图形式化提供了合理的逻辑基础。关健词：时序描述逻辑；统一建模语言顺序图；静态语义；动态语义；形式化规约；形式化验证FormalMethodofUMLSequenceDiagramBased0nTemporalDescriptionLogicCHENZhen-qing(DepartmentofComputerScienceandEngineering，HezhouUniversity,Hezhou5428

3、00，China)[AbstractlAccordingtothetemporalcharacteristicofUnifiedModelingLanguage(UML)sequencediagram，thispaperproposesaformalmethodofUMLsequencediagrambasedontemporaldescriptionlogicALCQIus．Thetemporalexpandsyntaxandsemanticsaregiven，thetheoremoftheassertionformulasofALCQIusisstu

4、died，theconsistencyreasoningalgorithmsisputforwardanditsdecidabilityisprovedthroughthestudyoftheassertionformulasofALCQIus．Takingthepublicsecurityalarmsystemasaexample，theformalspecific,ationandformalcheckingofUMLsequencediagramareexplainedthroughALCQIus，andtheALCQIusprovidesmore

5、reasonablelogicfoundationfortheformalizatiorLforUMLsequencediagram．[Keywords】temporaldescriptionlogic；UnifiedModelingLanguage(UML)sequencediagram；staticsemantic；dynamicsemantic；formalspecification；formalverificationDoI：10．3969／j．issn．1000-3428．2013．03．0081概述符扩展描述逻辑，提出了在时间段上受限的全称和

6、存在量统一建模语言(UnifiedModelingLanguage，UML)tll顺词。文献[4]对描述逻辑ALC进行了简单的时序扩展，加入了时态逻辑的时间点“Since”和“Until”运算符。这些时序图是一种重要的交互图，但由于缺乏精确的语义，不利于对其进行分析和验证。形式化方法是UML语义讨论的一序描述逻辑提供了有限的表达能力，无法满足UML顺序图个有效途径，包括PnueliA在内的诸多计算机科学家都认形式化的需要。文献[5-6】对描述逻辑DLR和ALCQI进行为采用形式化方法对系统进行验证是构造可靠软件的一个了时序扩展，分另0提出了DLRus和A

7、LCQIus，但没有给出重要途径【2j。描述逻辑是一阶谓词逻辑的可判定子集，具备具体的推理算法。文献[7]基于时序描述逻辑ALCT研究很强的知识表示和推理能力，是研究UML模型形式化方法UML顺序图的逻辑语义，但没有考虑顺序图的形式化验证的理想工具。UML顺序图对象间消息传递带有明显的时序问题。特征，而传统描述逻辑只能表达静态结构知识，无法表达针对上述问题，本文在文献[6-7]的基础上，提出了基时序特征，必须对传统描述逻辑进行时序扩展，才能满足于时序描述逻辑ALCQIus的UML顺序图形式化方法，研UML顺序图形式化方法研究的需要。文献[3]使用时间运算

8、究ALCQIus断言公式集一致性推理算法，以及UML顺序基金项目：广西壮族自治区