题目：基于模型检查的工作流的过程结构验证研究

工作流是一个运行的业务流程。工作流管理的目的是为了让合适的人或软件在恰当的时间执行正确的工作。它的主要特点是使处理过程自动化，使人和各种应用工具协同完成业务活动。一个工作流是正确的，通常包含三个方面，分别是语法正确、结构正确和语义正确。本文所讨论的是工作流的结构正确性。结构正确性是指工作流不存在结构异常，在执行过程中能够正常结束。目前，保证软件正确性的方法主要是通过软件测试。但是软件测试不仅资源耗费大，系统检查性也不够强。为了最早的发现问题，最直接的方法就是进行系统建模，模型分析和系统性质验证。模型检查是完全自动且高效的形式验证技术。经过二十多年的发展，成为了最成功的形式化自动验证技术之一。本文的研究目标是通过模型检查的方法对工作流的过程结构性质进行验证。本文的研究成果包括以下几个方面：利用UML内部包含的扩展机制，对UML活动图进行扩展，将UML建模与模型检查技术结合，允许用户在工作流中使用UML原模型不支持、而模型检查技术中特有的词汇来描述系统。文章给出了一种由改进的UML模型到PROMELA的转换方案。通过两者的结合，使得工作流建模既用户友好可视化又可通过模型检查技术确保其逻辑的正确性。为了更好的支持用户友好性，文章给出了一个友好的用户界面，该界面在Eclipse下开发，运行在Windows+SPIN+MinGW坏境下。根据给出的建模方案和转换方法，文章给出一个实例，并进行实验，并对实验结果进行了分析说明。在文章的最后，文章将本文提出的方法与其他进行了对比分析，更加明确了方案的相对优势。