基于构件的软件开发方法(Component-Based Software Development,简称CBSD)将外部开发的构件集成到具体应用环境中来构建面向特定应用的软件系统,不仅能提高生产效率,降低开发费用,还能显著提高软件的可靠性,已经成为当前软件领域的主流技术。在实时系统领域中,随着系统中软件规模和复杂度的迅速增加,整个系统的质量和可靠性极大地依赖于软件系统的实时行为。如何描述构件的动态行为,如何根据系统的功能、实时性和可信属性组装已有的构件以满足实时系统的应用需求,成为当前此领域的一个研究热点。形式化方法因其精确性和严格性,能较好的满足上述要求,CBSD与形式化开发方法的融合对于构造可信实时系统具有重要的理论价值和实际意义。形式化验证、充分的测试和有效的度量是主要的软件可信保证技术。本文将形式化方法和相应的模型检测工具、方法,以及可信质量模型相关理论应用于构件组装实时系统的构件建模、组装行为相容性验证、测试用例产生及构件选择,旨在构造一个可信的构件组装实时系统。本文的研究成果及核心内容归纳为如下四个方面：(1)提出一种基于时间自动机的实时构件模型RCM,并给出了RCM积的构造方法。采用形式化方法对实时构件的交互行为进行描述,对提高系统可靠性有重要意义。通过引入动作的定义对构件的交互行为建模,用时钟约束表示构件交互行为的时间约束信息,RCM可以利用时钟约束和复位的时钟集合限制实时构件交互行为；通过构件组合信息RCM可以体现体系结构的层次关系。RCM的优点是既提供对实时构件所特有的时间约束特征的语义描述机制,又提供对构件交互行为的形式化描述和体系结构信息描述。(2)提出一种对实时系统构件行为相容性分析验证的方法。基于构件的实时系统行为的不相容一般是由于时间约束不一致引起的,用RCM描述基于构件的实时系统,构件行为相容性问题就等价于在系统的实时模型上互补动作是否可以在共有通道上同步的问题,构件行为相容性检验可以转化为可被模型检测方法分析的可达性,最后用UPPAAL的验证功能给出结果。一个简单的铁路道岔系统的组装实例展示了这个方法及其效果。该方法的显著特点是建模精确,另外UPPAAL用动态验证技术和符号技术减少验证问题的规模,从而使该方法可以用于相当规模的系统组装。(3)提出了三个针对实时系统的测试用例覆盖标准,自动生成长度优化的测试用例并给出了实例分析。根据实时系统的特点,在满足组装行为相容性的前提下,针对实时系统的安全属性和时间属性这两个重要的可信属性定义了两个新的测试覆盖标准,针对重要组装行为定义了相容性覆盖标准,然后将这三个覆盖标准转化为模型检测工具UPPAAL中对性质进行描述的断言形式,最后利用UPPAAL工具的生成最短诊断路径的功能自动生成长度优化的测试用例。面向性质测试比非面向性质测试进行得更深入,因此,该方法产生的测试用例比传统的测试用例更高效、覆盖率更高。(4)提出了一种利用软件体系结构信息和可信等级化度量来选择构件并估计系统可靠性的方法。首先,根据构件软件及基于构件软件开发的层次性特征,用层次自动机对构件及整个软件系统进行形式化描述,用构件关系矩阵描述构件模块之间交互的频度,计算构件模块重要度因子,然后,根据重要程度不同,用重要度因子分级函数和等级质量映射函数来指导选择不同可信特性的构件组装系统并以此为基础对构件组装软件进行可靠性分析。最后,结合一个实例展示了这种方法的具体使用。构件组装相容性验证方法从行为层面指导构件选择,该方法更进一步,从属性量的指标层面来指导构件选择。该方法的显著特点是模型简单易理解,有效降低了系统复杂度。另外,引入不同的可信属性做为质量参数,使得构件的选择更加有效,为组装可信系统奠定了基础。