SOFL形式化规格说明向程序的自动转换

摘要

随着计算机科技不断发展，软件产品的应用越来越普及，因此保障软件质量和提高软件可靠性成为开发软件过程中值得关注的重要问题。形式化方法具有坚实的数学基础，拥有形式化规格说明和验证技术，这些逐步融入软件开发的各个阶段，是解决复杂系统开发中高可靠性问题的一个重要途径。SOFL(Structured Object-Oriented Formal Language)作为一种具有杰出代表的形式化方法，广泛应用于软件开发中。
　　SOFL不仅结合了多种传统的形式化方法，而且还采用了结构化流程和面向对象思想，继承了它们在软件系统开发中的优点。与此同时还集成了DFD(DataFlow Diagrams)、维也纳开发方法和Petri网络，形成了具有独特优势和有广泛应用前景的形式化方法。同时，由于其拥有独特的三步构建形式化规格说明机制和可控的条件数据流图，使用该方法可使软件开发在简单性、可视性和准确性达到良好平衡。
　　尽管SOFL已经应用在工业和研究项目中进行系统建模和设计，但是它并没有在工业软件系统开发过程中广泛应用，其中一个重要的原因就是缺乏有效的支持工具。因此研发出SOFL支持工具来促进其在软件产品研发领域中的应用，是非常必要的。基于以前的研究和工作，一个名为SOFL supporting tool的支持工具正在开发中。
　　本论文所研究的内容，将SOFL形式化规格说明自动转换为程序，作为SOFL支持工具的重要模块，发展和完善该工具，同时也可推进SOFL的发展和广泛应用，将其应用到实际的项目开发中。主要工作包括:
　　(1)分析SOFL规格说明的结构和框架，明确要转换的内容。比较SOFL语言和C#语言的相似和不同之处，综合对比两者语言，确定转换框架。
　　(2)研究SOFL规格说明中模块(module)的组成和内置数据类型(built-indata types)的结构以及具有的操作，选择合适的数据结构和算法，制定转换规则。
　　(3)构建抽象转换树，作为设计和实现整个系统的总纲。根据抽象转换树，绘制转换类图，设计接口和实现类，并根据以上研究和分析的转换准则来实现转换系统。
　　(4)对实现的自动转换系统进行测试，以验证系统功能的正确性，同时验证整个系统具有稳定、可靠的性能。

目录

声明

摘要

第一章 绪论

1．1 研究背景

1．2 国内外研究现状

1．2．1 国外研究现状

1．2．2 国内研究现状

1．3 研究目标和主要内容

1．4 论文的组织结构

第二章 形式化方法与SOFL语言

2．1 形式化方法

2．1．1 形式化规格说明(formal specification)

2．1．2 形式化验证(formal verification)

2．1．3 程序精化(Refinement)技术

2．2 形式化工程方法

2．3 SOFL简介

2．3．1 三步建立形式化规格说明机制

2．3．2 严格审查(Rigorous Review)技术进行验证和测试

2．3．3 与软件开发过程相结合

2．3．4 SOFL的局限性

2．4 本章小结

第三章 转换分析与设计

3．1 系统需求分析

3．2 系统整体框架

3．3 模块(module)转换分析

3．3．1 模块(module)简介

3．3．2 过程(process)结构和转换分析

3．3．3 模块转换原则设计

3．3．4 模块转化示例

3．4 数据类型(data type)转换分析

3．5 本章小结

第四章 系统实现

4．1 抽象转换树

4．2 实现系统框架

4．3 模块(module)转换实现

4．3．1 XmlTool类

4．3．2 ConstantTransformation类

4．3．3 TypeTransformation类

4．3．4 VariableTransformation类

4．3．5 FunctionTransformation类

4．3．6 ProcessTransformation类

4．3．7 ModuleDeclarationTransformation类

4．4 数据类型(data type)转换实现

4．4．1 基础数字类

4．4．2 set类

4．4．3 sequence类

4．4．4 map类

4．4．5 composite类和product类

4．4．6 union类

4．5 本章小结

第五章 系统测试

5．1 测试方案

5．1．1 测试目标

5．1．2 测试环境

5．1．3 测试方案

5．2 系统测试过程与结果

5．2．1 常量声明(constant declaration)转换测试

5．2．2 类型声明(type declaration)转换测试

5．2．3 变量声明(variable declaration)转换测试

5．2．4 过程声明(process declaration)转换测试

5．2．5 函数声明(function declaration)转换测试

5．2．6 模块(module)转换测试

5．2．7 测试总结

5．3 本章小结

第六章 总结和展望

6．1 本文工作总结

6．2 未来展望

致谢

参考文献