【作者】 王帆；

【导师】 梁洪峻；

【作者基本信息】 天津大学 ， 计算机软件与理论， 2004， 硕士

【摘要】 软件的规范说明阶段(specification phase)对于软件整体开发过程来说是一个非常重要的阶段，它可以被认为是需求分析的一部分。用自然语言来说明软件需求的优点是直观易懂、方便交流，但是会带来很多弊病，如二义性和不精确等。因此必须研究需求分析和规范说明技术以获得一致、完备和准确的软件规范说明书。形式化需求分析和软件规范说明技术就是在需求获取的基础上用建立系统的逻辑模型，从而对复杂实际问题进行分析和抽象、消除错误、去粗取精，最终将用户需求转化为软件规范说明的方法。软件系统的需求分析和规范说明阶段的多种方法和技术已被提出。这些方法大体上可被分为两类：形式化方法和非形式化方法。非形式化方法一般是采用图表的方式来描述系统。UML就是一种非形式化的方法，该方法是目前比较流行的软件工程开发方法，它对软件整体开发过程提供了一套有用的模型。UML方法已被广泛的应用于软件开发过程的各个阶段。被证明是一种行之有效的方法。但是它有所有非形式化方法所共有的缺点：表达的不严格和不精确，并且和规范的一致性和完整性不能被形式证明。本文为了解决UML的以上缺点，根据UML和谓词转换，以一阶逻辑和时序逻辑为基础提出一种面向对象的形式化规范说明方法，并给出一组和UML相对应的数学模型。本文的方法吸收了UML和一般形式化方法的优点，具有数学的严谨性和精确性，并且更加易于理解和表达。本软件规范说明方法的研究目标是使其能够最终实现目标代码的自动与半自动生成和程序的自动与半自动验证。更多还原

【Abstract】 The specification phase is of great importance to the whole process of the software development, which is always considered as part of the requirement system. Using nature language as specification method has many advantages, for instance it can be easily understood and the communion between the customers and programmer become easy. But it can also brings in a lot of disadvantages, for example nature language brings in misconception and imprecision. Consequently it is important to develop a precise method which can be used as a means of software verification. Formal specification is precise method by giving a mathematical model which provides laws to refine and verify the software. A great numbers of methods of requirements analysis and specification have been put forward, which usually can be categorized into two classes: The formal methods and informal methods. Informal methods generally describe a software system through tables and graphs. UML, as one of the informal methods, is very popular and has been proved as a effective through the process of software development.This paper put forward a formal method of software specification and a set of mathematics models, which is based on UML and the program semantics of predicate transformer. With the advantage of both UML and formal specification, Application of the method in this paper can be easily expressed and understood together with the mathematic rigorism.更多还原