随着计算机软件模型日趋复杂以及大规模与并发系统的应用，如何保证系统模型的正确性、一致性成为当前研究的热点。本课题以面向任务的系统集成设计方法为研究背景，该方法的建模特点是模型规模较大、结构复杂并且允许多人协同设计，因此有可能产生模型不一致现象。近年来，许多学者研究了使用形式化方法描述系统模型，并使用模型检测技术验证模型一致性的方法。然而现有方法仍然存在一些不足，比如：没有对类图、时序图和状态图之间由于模型重叠产生的一致性做出合适定义；在对复杂模型一致性的验证过程中，由于没有考虑冗余元素致使验证效率较低；现有将UML模型转换为PROMELA模型的方法无法验证某些视图、模型结构的一致性。针对上述不足，本文所做工作如下：首先，综合考虑UML类图、时序图、状态图的元素，结合模型的动态行为特征对行为一致性给出了新的定义；分析状态图中与一致性无关的冗余状态和迁移的特征，提出了针对无触发迁移、不可达状态、伪状态和复合状态的约简规则和状态图约简算法，实验表明该算法有效地降低了验证模型的复杂程度，减少了验证过程中状态和迁移数量，提高了验证效率。接着，针对当前的模型转换方法不完全支持时序图多条交互、时序图和状态图复杂结构以及行为一致性验证的不足，通过分析PROMELA的建模特征，提出了基于进程同步的UML模型到PROMELA转换方法，并设计了相应的模型转换算法。实验结果表明，该方法能够有效验证类图、时序图和状态图之间的行为一致性，并且支持类图，时序图多条交互、组合片段，状态图复杂结构。通过与现有文献中的六种模型转换方法进行对比，表明了该方法与现有方法相比在支持复杂模型结构和行为一致性验证方面具有一定优势。最后，根据状态图约简算法和基于进程同步的模型转换算法，在集成设计平台基础上设计并实现了系统设计工具，工具提供了系统建模及模型一致性验证等功能。使用该工具对“攻防系统”中进攻方系统进行建模及一致性验证，经验证模型中存在违反行为一致性的错误，并且根据模型检测工具产生的反例，修复了模型中的错误。