软件设计在软件工程的整个生命周期中所占的比重越来越大,合理正确的设计将会使后序的开发过程更加的稳定正确。同时,软件问题发现得越早,修复产生的代价就越小,因此软件设计的验证就成为了非常重要的部分。一方面由UML交互概观图和UML顺序图组成的UML交互模型是软件设计中常用的系统交互场景的建模语言,可以直观的描述系统的交互行为;另一方面,时间是交互系统的重要属性之一。因此,本文重点关注UML交互模型的时间性质的验证,以及在时间性质不满足时如何对时间约束进行修正。UML交互模型的时间性质验证属于模型检验的范畴,模型检验的一种思路是一次性计算出系统的所有状态空间,但是会有状态空间爆炸的缺点,计算量大,效率低。本文将整个模型检验分解为检验各个有界路径的方式,缩小了单次检验的复杂度和状态空间,提升了检验效率。同时,当有界路径中的时间性质不满足时,对时间约束进行修正。具体的工作成果如下:·提出了基于SAT-LP-IIS的UML交互模型的有界可达性检验方法。首先,本文采用布尔可满足性问题(Boolean satisfiability problem,SAT)的思路,将UML交互模型编码为合取范式,通过求合取范式真值解的方式求解有界路径。然后,对于路径中的时间约束,采用线性规划(Linear programming,LP)技术验证时间约束的满足性。当图模型规模很大时,本文采用了不可约简的不可解集技术(Irreducible Infeasible Subset,IIS)来进行加速处理。针对不可行路径,可以使用IIS技术找到其中的最小不可行路径片段,所有的包含该路径片段的路径均为不可行路径,之后的路径查找可以跳过这些路径,极大的提升了执行的效率。·针对时间性质不满足的路径,可能意味着UML交互模型存在着设计缺陷。本文针对不满足的时间约束提出了修正建议,即通过修正不可约简的不可解集使之可解,从而使时间约束变得满足。