形式化方法在构件组装实时系统中的应用研究

摘要
基于构件的软件开发方法（Component-Based  Software  Development，简称CBSD）将外部开发的构件集成到具体应用环境中来构建面向特定应用的软件系统，不仅能提高生产效率，降低开发费用，还能显著提高软件的可靠性，已经成为当前软件领域的主流技术。在实时系统领域中，随着系统中软件规模和复杂度的迅速增加，整个系统的质量和可靠性极大地依赖于软件系统的实时行为。如何描述构件的动态行为，如何根据系统的功能、实时性和可信属性组装已有的构件以满足实时系统的应用需求，成为当前此领域的一个研究热点。形式化方法因其精确性和严格性，能较好的满足上述要求， CBSD 与形式化开发方法的融合对于构造可信实时系统具有重要的理论价值和实际意义。形式化验证、充分的测试和有效的度量是主要的软件可信保证技术。本文将形式化方法和相应的模型检测工具、方法，以及可信质量模型相关理论应用于构件组装实时系统的构件建模、组装行为相容性验证、测试用例产生及构件选择，旨在构造一个可信的构件组装实时系统。本文的研究成果及核心内容归纳为如下四个方面:
（1）提出一种基于时间自动机的实时构件模型 RCM，并给出了 RCM 积的构造方法。采用形式化方法对实时构件的交互行为进行描述，对提高系统可靠性有重要意义。通过引入动作的定义对构件的交互行为建模,用时钟约束表示构件交互行为的时间约束信息，RCM 可以利用时钟约束和复位的时钟集合限制实时构件交互行为；通过构件组合信息 RCM 可以体现体系结构的层次关系。RCM的优点是既提供对实时构件所特有的时间约束特征的语义描述机制，又提供对构件交互行为的形式化描述和体系结构信息描述。
（2）提出一种对实时系统构件行为相容性分析验证的方法。基于构件的实时系统行为的不相容一般是由于时间约束不一致引起的，用 RCM 描述基于构件的实时系统，构件行为相容性问题就等价于在系统的实时模型上互补动作是否可以在共有通道上同步的问题,构件行为相容性检验可以转化为可被模型检测方法分析的可达性，最后用 UPPAAL 的验证功能给出结果。一个简单的铁路道岔系统的组装实例展示了这个方法及其效果。该方法的显著特点是建模精确，另外UPPAAL 用动态验证技术和符号技术减少验证问题的规模，从而使该方法可以用于相当规模的系统组装。
（3）提出了三个针对实时系统的测试用例覆盖标准，自动生成长度优化的测试用例并给出了实例分析。根据实时系统的特点，在满足组装行为相容性的前提下，针对实时系统的安全属性和时间属性这两个重要的可信属性定义了两个新的测试覆盖标准，针对重要组装行为定义了相容性覆盖标准,然后将这三个覆盖标准转化为模型检测工具 UPPAAL 中对性质进行描述的断言形式，最后利用UPPAAL 工具的生成最短诊断路径的功能自动生成长度优化的测试用例。面向性质测试比非面向性质测试进行得更深入，因此，该方法产生的测试用例比传统的测试用例更高效、覆盖率更高。
（4）提出了一种利用软件体系结构信息和可信等级化度量来选择构件并估计系统可靠性的方法。首先，根据构件软件及基于构件软件开发的层次性特征，用层次自动机对构件及整个软件系统进行形式化描述,用构件关系矩阵描述构件模块之间交互的频度，计算构件模块重要度因子，然后，根据重要程度不同，用重要度因子分级函数和等级质量映射函数来指导选择不同可信特性的构件组装系统并以此为基础对构件组装软件进行可靠性分析。最后，结合一个实例展示了这种方法的具体使用。构件组装相容性验证方法从行为层面指导构件选择，该方法更进一步，从属性量的指标层面来指导构件选择。该方法的显著特点是模型简单易理解，有效降低了系统复杂度。另外，引入不同的可信属性做为质量参数，使得构件的选择更加有效，为组装可信系统奠定了基础。
关键词：形式化方法，构件组装实时系统，时间自动机，行为相容性，测试用例生成，构件选择
目录
摘要  .....................................................  I
Abstract  ...............................................  III
1  绪论  ..................................................  1
1.1  研究背景和意义  .............................................  1
1.2  研究问题  ...................................................  2
1.3  研究内容  ...................................................  3
1.4  本文篇章结构  ...............................................  4
1.5  本章小结  ...................................................  6
2  CBSD 研究综述 .........................................  7
2.1  基于构件的软件开发方法  .....................................  7
2.1.1  概述  ..........................................................  7
2.1.2  CBSD 的发展过程  ...............................................  8
2.2  构件  .......................................................  9
2.2.1  构件的概念  ....................................................  9
2.2.2  实时构件的基本特征  ...........................................  10
2.2.3  主流构件技术和模型  ...........................................  12
2.2.4  可信构件的相关研究  ...........................................  14
2.3  构件组装技术  ..............................................  18
2.3.1  构件组装方式和构件组装技术  ...................................  18
2.3.2  构件组装开发实践  .............................................  19
2.4  形式化方法  ................................................  21
2.5  模型验证技术  ..............................................  24
2.5.1  模型检测  .....................................................  24
2.5.2  模型检测工具  .................................................  26
2.6  本章小结  ..................................................  28
3  构件建模和构件行为相容性  .............................  30
3.1  问题背景  ..................................................  30
3.2  构件模型及时间行为的形式化描述  ............................  31
3.2.1  构件模型及构件行为的形式化描述  ...............................  32
3.2.2  时间行为形式化描述方法  .......................................  33
3.3  时间自动机和 UPPAAL........................................  34
3.3.1  时间自动机  ...................................................  34
3.3.2  UPPAAL 介绍  ..................................................  38
3.4  实时构件的建模  ............................................  40
3.5  构件行为相容性分析  ........................................  42
3.5.1  常见相容性错误  ...............................................  42
3.5.2  不相容的构件行为在 RCM 模型上的形式化表示  ...................  43
3.5.3  构件行为相容性验证  ...........................................  43
3.6  实例分析  ..................................................  45
3.7  相关工作比较  ..............................................  54
3.8  本章小结  ..................................................  54
4  实时系统测试用例产生  .................................  56
4.1  问题背景  ..................................................  56
4.2  测试用例生成方法  ..........................................  59
4.2.1  主流的测试用例生成方法  .......................................  60
4.2.2  形式模型  .....................................................  61
4.2.3  基于模型的实时系统测试用例生成方法  ...........................  62
4.2.4  基于模型检测的测试用例产生  ...................................  66
4.3  新的测试覆盖标准和长度优化的测试用例产生  ..................  66
4.3.1  测试用例覆盖标准  .............................................  66
4.3.2  生成长度优化的测试用例  .......................................  69
4.4  实例分析  ..................................................  71
4.5  相关工作比较  ..............................................  75
4.6  本章小结  ..................................................  76
5  构件选择及组装可靠性分析  .............................  77
5.1  问题背景  ..................................................  77
5.2  构件选择和构件可靠性模型  ..................................  79
5.2.1  构件选择的模型  ...............................................  79
5.2.2  构件选择的方法  ...............................................  80
5.2.3  构件的评价方法  ...............................................  80
5.2.4  构件可靠性模型  ...............................................  81
5.2.5  构件选择的其他研究问题  .......................................  82
5.3  层次自动机  ................................................  82
5.4  构件的层次自动机模型  ......................................  84
5.5  构件选择及组装可靠性分析  ..................................  84
5.5.1  构件关系矩阵和重要度因子  .....................................  84
5.5.2  用软件可信等级化度量方法选择服务构件  .........................  86
5.5.3  构件软件系统的可靠性  .........................................  87
5.6  实例分析  ..................................................  89
5.7  相关工作比较  ..............................................  91
5.8  本章小结  ..................................................  92
6  结论与展望  ...........................................  94
6.1  论文工作总结  ..............................................  94
6.2  进一步工作  ................................................  95
参考文献  ................................................  97
致谢  ...................................................  110