UML交互模型的时间性质验证及修正技术研究

来源 :南京大学 | 被引量 : 0次 | 上传用户:zldzhang
下载到本地 , 更方便阅读
声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架
论文部分内容阅读
软件设计在软件工程的整个生命周期中所占的比重越来越大,合理正确的设计将会使后序的开发过程更加的稳定正确。同时,软件问题发现得越早,修复产生的代价就越小,因此软件设计的验证就成为了非常重要的部分。一方面由UML交互概观图和UML顺序图组成的UML交互模型是软件设计中常用的系统交互场景的建模语言,可以直观的描述系统的交互行为;另一方面,时间是交互系统的重要属性之一。因此,本文重点关注UML交互模型的时间性质的验证,以及在时间性质不满足时如何对时间约束进行修正。UML交互模型的时间性质验证属于模型检验的范畴,模型检验的一种思路是一次性计算出系统的所有状态空间,但是会有状态空间爆炸的缺点,计算量大,效率低。本文将整个模型检验分解为检验各个有界路径的方式,缩小了单次检验的复杂度和状态空间,提升了检验效率。同时,当有界路径中的时间性质不满足时,对时间约束进行修正。具体的工作成果如下:·提出了基于SAT-LP-IIS的UML交互模型的有界可达性检验方法。首先,本文采用布尔可满足性问题(Boolean satisfiability problem,SAT)的思路,将UML交互模型编码为合取范式,通过求合取范式真值解的方式求解有界路径。然后,对于路径中的时间约束,采用线性规划(Linear programming,LP)技术验证时间约束的满足性。当图模型规模很大时,本文采用了不可约简的不可解集技术(Irreducible Infeasible Subset,IIS)来进行加速处理。针对不可行路径,可以使用IIS技术找到其中的最小不可行路径片段,所有的包含该路径片段的路径均为不可行路径,之后的路径查找可以跳过这些路径,极大的提升了执行的效率。·针对时间性质不满足的路径,可能意味着UML交互模型存在着设计缺陷。本文针对不满足的时间约束提出了修正建议,即通过修正不可约简的不可解集使之可解,从而使时间约束变得满足。
其他文献
加工工业是我国国民经济发展和进步的重要推动力,在过去的数十年间加工工业取得了稳定的发展,为提供更多人们生活需求产品做出了突出贡献。但是,我们不得不承认的是,随着中国
<正>当前群团改革的新形势要求团组织进一步跳出"就团论团"的模式,解放思想,大胆调整团的组织设置,构建新的运行机制,优化团的资源配置,走社会化之路,推进团的各项事业。在群
【正】经鼻气管插管是指将一导管插入鼻腔内建立的气体通道,纠正患者的缺氧状态,改善患者的通气功能,有效地清除气道内分泌物,与多功能呼吸机连接可监测通气量,呼吸力学等参
全人教育注重促进学生全面发展,具有课程体系丰富、教学模式多样、评价体系完善等多种优势,对民办高校思政课教育具有启示作用和借鉴意义。因而思政课教育教学活动中要树立全
由于具有工作电压高、工作范围宽、比能量大、无污染、使用寿命长等优点,锂离子电池具有广阔的应用前景。然而,目前商业化的锂离子电池仍无法满足电动汽车对电池低成本及高能
魏晋时期是中国书法史上新旧书风的交替期,在新旧书风相互影响的环境中,铭石书的形态也发生了前所未有的变化。在新书风繁盛的东晋,这种新旧混杂的现象在铭刻书迹中表现很突
目的探讨孤独症儿童母亲一般自我效能感、社会支持与亲职压力的特点及其相关性,以采取针对性措施促进孤独症患儿母亲心理健康,利于患儿康复。方法采用&#39;亲职压力量表&#39;
Cu-ZSM-5分子筛因具有高的催化脱除NO活性和对环境友好等优点而引起广泛关注。本文从NO分解反应、以NH3为还原剂选择性催化还原NO(NH3-SCR-NO)和以碳氢化合物为还原剂选择性
船舶操纵模拟器在船员教学、培训、评估考试中应用广泛。文中介绍了实用型船舶操纵模拟器的组成、功能及特色,并对它在内河船员和海船船员的教学培训应用、技术开发、双师型
自顺铂临床用于抗肿瘤药物以来,在铂配合物中寻找新的药物已成为研究的热点,现已有顺铂、卡铂和奥沙利铂广泛应用于临床。根据经典的构效关系,上千个新的铂类化合物被设计与