论文部分内容阅读
形式化方法目前在工业界还没有得到广泛应用，主要是因为各种形式化方法没有很好地整合到工业界的软件开发过程中去，并且目前还没有比较成熟的形式化工具可以对软件开发提供令人满意的支持。在这个背景下，SOFL作为一种更贴近工业界软件开发需要的形式化工程方法被提出来。它结合了传统的形式化方法以及结构化方法和面向对象方法。SOFL集成了数据流图、Petri网络以及VDM形式化规格说明语言，形成了一套全新的形式化方法。
形式验证是形式化方法的一个重要组成部分。形式验证主要分为定理证明、模型检测和形式化测试三种方法。SOFL的形式验证主要采用测试的方法，分为单元测试和集成测试。本文主要讨论SOFL理论中的集成测试理论。包括以下几个主要方面：
①针对数据流图内各元素之间的一致性测试，研究如何统一Proof Obligation的生成策略。我们在文章中给出了一种通过分类和简化CDFD图形结构的方式来构筑统一的Proof Obligation生成策略。
②探索如何有效地完成数据流图之间的一致性测试。CDFD的图形结构和图形元素非常复杂，我们很难找到一个统一的算法来生成CDFD间一致性测试的Proof Obligation。本文提出了通过一种实现形式验证的方法：通过输入CDFD的输入数据计算CDFD输出数据，根据对输出数据的分析进行验证。
③结合SOFL的测试策略，研究如何引导用户进行对形式化规格说明的集成测试。针对这一问题，本文提出了分层引导测试的测试模式。使用分层引导测试，用户可以在工具的配合下充分遍历SOFL形式化规格说明测试的所有测试标准，从而提高SOFL形式验证的检错效率。
作为整个SOFL形式化方法支撑工具的一部分，本文还简要介绍了当前SOFL集成测试工具的开发情况。目前，工具的开发还处在原型阶段，还有大量的理论问题急待解决。为继续当前的理论研究和工具开发，还需要解决以下几个主要内容：
（1）进一步深化数据流图一致性测试的相关研究，并最终完善快速、便捷的Proof Obligation的生成算法。（2）深化对SOFL复杂数据类型的研究，以使工具支持复杂数据类型的测试。（3）进一步深化测试模型的研究，并最终寻找一条自动生成测试用例的可行之路。