【作者】 席琳；

【导师】 周清雷；

【作者基本信息】 郑州大学 ， 计算机软件与理论， 2012， 博士

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

【Abstract】 With the growth of software scale and complexity, the quality and reliability of the whole real-time system greatly depend on the efficient software development technique. These are strong motivations to apply new software engineering technique—Component-Based Software Development(CBSD).Component-Based Software Development represents a pattern of "reuse instead of reinvention". It shifts the emphasis on software development from scratches to reusing and assembling of ready-made components and has become mainstream in software technique domain due to its lower cost, shorter time and higher reliability. Nowadays, how to describe the dynamic behavior and how to composite ready-made components for application according to the system’s function, real-time property and trustworthy attributes have become hot-topics in research domain, and formal method can satisfy the above demands well for its accuracy. Thus, a novel concept to combine CBSD and formal method for constructing trustworthy real-time system is introduce in this paper.Formal verification, adequate test and effective measurement are main trustworthy guarantee technique. So, formal methods, their corresponding model checking techniques and the theories of quality model of trusted component is applied to component modeling, verification of behavioral compatibility, test generation and component selection in thie thesis, aiming to construct a trustworthy component-based real-time system. The main contributions of this thesis are as follows:(1) This thesis gives a formal model of real-time component based on timed automata(TA) named RCM, and also how to construct the product of the RCM is introduced. The behavior of components is modeled by introducing the definition of "Action" and the time property is shown by clock constraint in the RCM. So the model can limit the behavior of real-time components by clock constraint and the set of clock to be reset. RCM can also indicate the composition relation of components. The advantage of the RCM is that it provides description of real-time property, dynamic behavior between components and the architecture information.(2) This thesis proposes a technique for behavioral compatibility analysis of component-based real-time system. The behavioral incompatibility of real-time system is often due to the inconsistency of clock constraints. So, how to describe and verify such behavioral incompatibility in an effective way should be taken more into consideration in real-time system component composition. First, the RCM based on timed automata is used to formally describe the component. In this way, the problem of component behavioral compatibility is equivalent to whether the complementary actions can really synchronize over common channels on the system’s models. Then, the formulation of the behavioral compatibility verification is enabled as reachability properties that can be checked by reachability analysis of the model, and the verification function of the UPPAAL tool is used to generate the result. Finally, the method is applied to the composition of the railway level crossing control system, the results demonstrate the effectiveness and performance of the proposal. The obvious advantage of this method is the model of the component is explicit and the method is useful in sizeable component-composition systems, because model checking is often hampered by various state explosion problems, and in UPPAAL these problems are dealt with by a combination of on-the-fly verification together with a new and coarser symbolic technique reducing the verification problem to that of solving simple linear constraint systems.(3) This thesis introduces new coverage criteria and the method to automatically generate length optimal tests for real-time system. On the basis of behavioral compatibility, new coverage criteria concerning safety, time property and key behavioral compatibility for the abstract formal of real-time system are presented and enabled as reachability properties. The method makes use of the RCM to formally describe the real-time system and uses the length optimal reachability feature of UPPAAL to automatically generate length optimal test sequences for the new coverage criteria. Experiment demonstrates how the technique works and performs. In general, testing focusing on particular properties is effective, so tests generated in this method have higher coverage and efficiency than traditional ones.(4) This thesis provides a method for component selection and system reliability calculation. First, according to the hierarchy character of component-based software development, it makes use of the Hierarchical Automata(HA) to describe the component modules and the whole service system. Based on the interaction frequency among component modules, the relation matrix is introduced to calculate the importance factors contributing to the whole system. Wherein, to meet the system design requirement, a many-to-one mapping function is used to rank the importance into difference levels, each level corresponds to different quality criteria, which in return is used to select the appropriate components. Then, it proposes an algorithm to calculate the resulting system reliability. Finally, it studies a case to demonstrate the selection of components and the estimation of resulting reliability. Behavioral compatibility analysis of component-based system instructs component selection from behavior level, further more, this method from quality metrics. The obvious advantage of this method is that the model is easy to understand. Meanwhile, different trustworthy attributes are used as quality parameters, making the component selection and composition of the trustworthy software more effective.更多还原