题目：基于Petri网的UML状态机模型的形式化验证方法研究

随着软件工程技术的发展，UML成为可视化建模语言事实上的工业标准，因此在工业界、学术界被广泛承认与采用。在世界范围内，UML更是面向对象技术领域内占主导地位的标准建模语言。然而，在UML取得巨大成功的同时，在某些特定应用中仍存在一些问题，例如在高可靠性领域，用户因关键模型的语义不确定性而面临开发系统的质量和性能的巨大挑战，而状态机在这类系统的开发当中被大量使用，所以就亟需一种机制来验证状态机模型的正确性。Petri网既是一种图形化建模工具，又是具有严格的语法和语义定义的形式化方法，不但能有效地对系统进行描述和建模，对系统的并发性、异步性和不确定性也有很强的动态分析能力。论文通过将UML状态机模型转化为Petri网模型，再利用Petri网的分析验证技术，可以实现对状态机模型的正确性的验证。这样就可以在设计阶段发现系统的缺陷，从而减少软件开发后期才发现设计的错误而带来的损失，保证了系统的正确性和安全性。论文首先给出了UML状态机的定义，下来对状态机的语义进行了充分的研究，为后面状态机到Petri网的转化做基础工作，主要研究状态机运行过程的状态活动语义、转换活动语义和冲突转换的优先级。然后在UML状态机到Petri网的转化过程中，完善了UML状态机到平面模型的转化方法，这种方法的目的是去掉复合状态和复杂转换，得到平面模型FM，下来介绍了平面模型到Petri网的转换方法，在这个过程中提出了转换事件结构TES，给出了复合转换的转化方法和平面模型到Petri网的转化规则，并在理论和语义上分析了转化方法的正确性。接下来给出了原型系统的设计和实现方法，最后给出几个用Petri网验证状态机模型的实例。经过实验证明，论文研究成果有一定的理论和实用价值，可以在很大程度上验证状态机模型中的错误。