论文部分内容阅读
多年以来，形式化规约(formal specification)一直是软件工程领域中的一个研究热点，它的应用范围也正在逐步增长。许多研究表明，对形式化规约的错误检测能够大幅度减少软件工程项目的成本和风险。SOFL(Structured Object-oriented Formal Language)是针对形式化方法在软件工程实践中的应用而提出的形式化工程方法。本文针对SOFL形式化规约，提出了基于特性的形式化规约复审方法，并讨论了支撑工具的研究和开发。
本文分析了形式化工程方法SOFL和复审技术，针对形式化的SOFL规约，提出了三个面向不同方面的复审视图，并从不同的视图分析形式化规约复审中需要把握的特性，并说明了相应的复审方法、策略。
本文着重在面向过程的严格复审方法中，采用复审任务树技术，提出了基于特性的SOFL形式化规约复审方法。本文讨论了基于特性的形式化复审的一般步骤，并对关键特性的提取，复审任务树的生成和复审任务的评估进行了分析，还提出了基于模块层次结构的复审策略。
在此基础上，我们设计和开发出形式化规约复审工具，帮助复审者有效地完成复审任务，提供对SOFL形式化规约的复审支持，同时还将集成到SOFL形式化方法的智能开发环境中。