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