统一建模语言(Unified Modeling Language,UML)作为面向对象的分析与设计方法的代表,已经获得了广泛的关注和研究,并在多个领域中有成功的应用。然而,由于UML作为一种符号化语言系统,其语义采用自然语言描述,缺乏精确的语义描述,因此,难以对UML模型进行分析验证以判断设计规范是否满足目标需求。模型验证是一种能够有效保证系统可信性质的自动验证技术,已被广泛地应用于工业界。如何将UML与模型验证二者有效的相结合,从而避免系统设计中的错误,提高软件的生产效率和质量已成为软件工程领域的研究热点。简单进程元语言解释器(Simple PROMELA Interpreter,SPIN)作为模型验证的一种开源工具,由于具有占用内存空间小,并保证程序能够按照原有的工作方式被高效地验证的特点,被普遍地应用于工业界和学术界,因此,本文主要研究基于SPIN的UML模型验证技术。论文首先介绍了形式化验证的方法,以及模型验证技术的原理、特点和过程,对模型验证工具SPIN的原理、输入语言PROMELA和优化技术作了详细的阐述;其次,通过对UML模型的结构和特点的分析,选取UML中类图、状态机图和协作图作为系统描述模型,根据验证的需要,结合类图和状态机图作为验证模型;然后,基于同态映射的方法,给出了UML验证模型到PROMELA模型的转换方法,并使用层次自动机描述状态机,定义了其形式化语义,将状态机图和类图的信息表示为相应的PROMELA模型,将UML的协作图信息描述为LTL公式并作为系统约束,使用模型验证工具SPIN验证UML模型所描述系统的正确性;最后,基于上述研究工作,设计并开发了UML模型自动转换验证工具UML2PROMELA。