【作者】 王博；

【导师】 陈文光；

【作者基本信息】 清华大学 ， 计算机科学与技术， 2016， 博士

【摘要】 现代嵌入式系统广泛应用于航空、航天、工业控制、民用电子等领域。随着嵌入式软件规模和复杂度的不断增长,基于构件的设计技术逐渐得到广泛应用,通过测试保证构件功能和集成构造的正确性、软件运行时序的正确性、以及运行健壮性等成为重要的研究问题。本文采用基于模型的测试思想,建立了嵌入式软件的可组合接口模型,在此基础上提出一套构件测试和时序测试生成方法、以及异常时序检测方法,提升了测试的自动化和系统化程度,提高了测试生成的质量和效率,为提高嵌入式软件测试有效性和测试质量提供新的途径。在嵌入式软件建模方面,提出接口语义自动机(Interface Semantic Automata,ISA)模型,通过引入语义规则,从行为、时序两个方面增强和扩展模型的语法、语义表达能力。在ISA模型中,定义了接口行为参数、中间变量,建立了基于谓词逻辑的行为约束,通过模型的可组合性和组合操作,支持构件间的集成测试。针对嵌入式软件的时间需求,定义了时间变量、置零行为、以及典型时间约束,支持运行时序的定量描述。ISA模型为构件和时序测试提供了设计信息和领域知识。在嵌入式构件测试研究中,提出基于符号执行的构件测试生成方法。在嵌入式软件ISA模型之上,利用动态符号执行技术,搜索生成有效的事件/行为序列,构建测试路径集,进而沿特定测试路径采用基于相关性分析的约束求解方法生成测试数据。针对各类功能异常,提出基于约束条件变异、基于插桩以及基于反例的测试方法,对构件的功能异常处理机制进行测试。在构件功能验证基础上,提出基于构件间组合路径的集成测试方法,生成集成测试用例。在时序测试研究中,提出基于时间约束相关性分析的分区测试方法。通过分析、识别和提取相关时间变量间的取值依赖关系,针对各项独立、相关时间约束,划分相应时间变量的有效测试分区,并在测试分区内抽取典型时间数据,对各类正常、异常运行时序进行测试。针对软件测试中难以发现的运行时序故障,提出一种基于执行序列的异常时序检测方法,通过提取包含时间信息的执行序列,检验其是否满足ISA模型描述的时间需求,进而发现软件存在的时序缺陷。本文以列车通信网络实时通信协议软件、卫星定位终端软件为被测对象,进行构件和集成测试、以及时序测试工作实践。测试结果显示,本文方法可有效发现各类构件功能和集成故障、以及运行时序故障,提高了嵌入式软件测试的质量。更多还原

【Abstract】 Embedded systems have been widely used in many fields such as aviation,aerospace,industrial control,civil electronics and so on.With the growing scale and complexity of embedded software,Component-based technology gains increasing attentions in embedded software design and development,which introduces new quality concerns including the stability of components and their compositions,temporal correctness,and runtime robustness.Following the Model-Based Testing(MBT)approach,the thesis proposes a composable interface model for embedded software,and the methods for automatic testing and verification based on the interface model.The methods and algorithms facilitate systematic automatic testing,which enhance the quality,effectiveness,and efficiency of test generation.The thesis proposes an Interface Semantic Automata(ISA)for embedded software,and the syntax and semantic are extended for modeling of behavior and temporal properties.ISA defines parameters of interface operations,internal variables,and constraints using predicates in first-order logic,which are used for components composability analysis and integration testing.ISA also defines time variables,reset actions,and timing constraints,which can be used to describe the timing requirements quantitatively for temporal testing.Based on ISA,symbolic execution algorithms are designed for traversing the model and generating test cases.Metrices are defined for ISA structural and data coverage.Dynamic symbolic execution is used to search and generate valid event/behavior sequences to construct the suit of test path,and test datas are generated using constraint solving based on correlation analysis along specific test path.For robustness testing,abnormal inputs are generated using constraint inversion,stubbing and counterexample,to verify exception handling mechisms.Then an integrated test method is proposed according to the component integration path.A partition test method is proposed based on correlation analysis of timing constraints.The correlations of timing constraints are analyzed,and value dependencies between corresponding time variables are extracted.Base on that,input domains of time variables are divided into equivalent partions for specific independent or related timing constraints,and temporal datas are sampled on them for temporal testing.In addition to testing,temporal behaviors are also verified by analyzing execution traces to find runtime defects that are hard to be detected in simulation environment.Execution traces are logged and tagged with time properties,and checked against ISA model of their conformance to ISA specified timing requirments.The proposed methods are applied on component and integrated testing of a RTP(Real Time Protocol)software of high-speed railway communication network and temporal testing of a SPT(Satellite Positioning Terminal)software.The results show that the proposed methods can effectively find various functional,integration,and temporal defects,which enhance the quality of embedded software testing.更多还原