论文部分内容阅读
随着工业的飞速发展、信息技术的不断进步，计算机信息系统在各个行业得到广泛应用。保证软件可靠性，提高软件的质量是软件研究的重要组成部分。目前，根据工业需求复杂度和规模的增加，软件系统的规模和业务逻辑逐渐增加，出现软件需求前后逻辑不一致的情况增多，造成开发的软件具有许多安全隐患。因此，保证软件需求前后逻辑一致性是保障软件可靠性，提高软件的质量的重要途径。在软件开发流程中引用形式化分析方法进行需求分析，检验软件需求前后逻辑一致性是提高软件质量的有效方法。 UML是当前软件开发中最为流行的可视化建模语言，已在软件的分析和设计中得到了普遍的应用。由于UML是半形式化的描述语言，多数描述采用自然语言，使UML模型缺乏精确的语义，容易产生理解分歧。另外，UML本身缺乏完善的模型检查能力和有效的验证、推理机制。软件形式化分析方法以数学为基础，能够对目标建立无二义性、精确的语义。但是形式化方法由需求直接构建形式化描述比较困难，使得目前软件分析形式化方法的研究特别是使用仍然局限在较小的范围中。B方法是一种软件形式化分析方法，通过严格的推理和证明发现需求前后逻辑不一致的问题。根据B方法的具体模型接近于计算机的表达方式，B的具体模型容易开发出软件代码自动生成工具，并在工业中得到了广泛的应用。本文提出的基于B方法的软件UML形式化分析方法，通过将UML模型图转换为B方法的抽象模型，得到UML形式化分析方法，即能根据抽象模型对需求进行形式化证明，又能降低由需求文档直接得到B方法抽象模型的使用难度，因此，基于B方法的软件UML形式化分析模型更具有效率，提高需求分析中的可靠性，保证软件的质量。 本文在分析研究软件开发中的UML建模和形式化分析方法的基础上，在UML形式化分析方面进行研究，作了如下研究工作： 1、提出了基于B方法的UML形式化分析模型。根据UML易于使用、图形化建模的特点，将UML模型图转化为B方法的抽象模型，运用B方法的逻辑证明方法，及时发现需求分析中的不一致性，以便降低设计中出现问题的风险。并且由UML模型图转换为B抽象模型降低了由需求分析直接得到B抽象模型的难度，提高了形式化分析的效率。 2、本文研究了UML类图、用例图转换为B抽象模型的方法。根据面向对象中类和B方法中的抽象机的相似性质、类之间的关系和B方法中的抽象机组织机制的相似性，实现类图到B方法的转换；将UML中的参与者、用例看作特殊的类从而实现用例图到B方法的转换。 3、运用本文提出的UML形式化分析模型对订单系统进行实例分析。详细介绍模型的应用方法，并利用B方法工具Atelier B对系统进行逻辑证明，以发现在该系统需求分析前后逻辑定义不一致的问题。