统一建模语言(Unified Modeling Language,UML)是一种描述能力强大且含义直观的可视化建模语言,它提供多种视图从不同角度和应用层次刻画系统特性以及复杂的运行环境。UML语法结构虽然采用了形式化的规约,但其语义部分则是用自然语言来描述。容易产生模糊或歧义。因此,对UML进行形式化语义研究,可以增进该语言的准确性、一致性和可扩展性。UML2.0版本的顺序图经常用于描述并发系统的设计需求,反映对象之间的动态交互关系,着重体现对象之间消息传递的时间顺序,因此,用一个恰当的时序逻辑描述语言来给出它的语义是可行的。XYZ/E是一种可执行的线性时序逻辑语言,既可描述系统的动态行为又可表示程序性质,对顺序图进行形式化规约后,可在统一的时序逻辑框架下分析顺序图的性质。论文给出了一个改进的顺序图语法定义,同时对现有的基于XYZ/E时序逻辑语言的UML顺序图语义进行了深入研究,针对存在的问题,根据给出的语法定义,提出了新的解决方案,更加精确地描述了顺序图的语义。UML支持用户从不同的角度对系统建模,不同视图间存在着信息的冗余,如顺序图和状态图在描述动态行为上存在着重叠,因此可能导致视图间不一致的产生。首先,论文介绍了形式化模型检验方法的原理和特点,阐述了模型检验工具SPIN的原理和语法。其次,针对顺序图逻辑语义多样性的特点,提出了一种分析方法,同时给出了新的语义定义。再次,提出一个更全面的状态图语法定义,并针对状态图的复杂层次结构特性,引入有限状态自动机,提出自动机分解算法FSADA,经分解后得到自动机树。最后,提出新的顺序图和状态图的一致性检验准则、Promela代码结构,以及将状态图转换成Promela代码的ATTP算法,并用模型检验工具SPIN实现了两者之间的一致性检验。