uml用例模型b形式化描述方法研究.pdf

论文题目： UML用例模型的B形式化描述方法研究 专 业： 计算机应用技术 硕士生： 段建荣 (签名) 整堑盘 ’， 指导老师： 高晔 (签名) 3鲜 I 摘 要 随着信息技术的飞速发展，计算机软件系统的应用逐渐扩展到了社会的各个领域。 软件规模和复杂度在不断增加，软件出现错误的可能性也随之增加。如何保证软件的质 量、提高软件的可靠性，已成为目前软件工程研究领域的一个热点。将形式化方法和主 流的软件开发方法相结合是一种可行的方法。 UML作为当前比较流行的一种可视化建模语言，己成为面向对象分析和设计中事 实上的工业标准。UML模型直观、易懂，利于开发者与用户之间的沟通。但UML的大 部分语义是用自然语言描述的，确乏精确的语义，容易产生模糊或歧义；UML缺乏有 效的推理机制和完善的模型检查能力，不便于使用工具对其描述的规约进行动态分析和 验证。形式化方法则是基于严格数学理论的，能产生精确、无二义性的形式规约，为软 件开发提供了严格的数学基础，这对提高软件的可靠性有着非常显著的作用。但形式规 约不够直观，可读性较差，不便于与用户进行交流，要求开发者具有良好的数学基础。 因此，形式化方法的研究和应用目前仍局限在较小的范围之内。把形式化方法和UML 相结合实现优势互补的研究对保证软件质量、提高可靠性有着非常重要的意义。 本文选择B方法作为形式规约方法，把UML模型的图形规约映射到B形式规约。 一方面，我们能够借助于强大的B方法支持工具，基于相应的B形式规约，对UML建 模结果进行J下确性分析和一致性检查；另一方面，可将UML规约作为形式化开发的基 础，降低直接使用B方法建立形式规约的难度，增强B方法在软件开发中的实际作用。 本文以UML用例模型为主要研究对象，在分析UML用例模型概念和B抽象机符 号的基础上，对用例模型建模元素的抽象语法进行描述，建立两者之间的映射，实现 UML用例模型图到B形式规约的转换。软件开发人员可以首先用半形式化的UML用 例模型为目标系统建立需求模型，然后根据文中给出方法构建目标系统的B形式化规 约，再利用B方法支持工具对规约进行动态分析和模型验证，得出可靠的形式规约，为 在此基础上进行的形式推导和精化提供了正确的起点。最后，通过对电梯控制系统的实 例分析，进一步详述了UML用例模型到B方法形式规约的转换方法及过程，并利用B 方法的支持工具ProB对所得到的形式化模型进行了动态分析和模型检测。 关键词：形式化方法；B方法；抽象机；UML；用例模型；ProB 研究类型：应用研究型 ：TheResearchOilB Subject Formal ofUMLUseCase Specification Model ： Specialty ComputerApplication Technology Name：Duan Jianrong (signature) Instructor：GaoYe (signature) ABSTRACT With of information rapiddevelopment of technology，theapplication