Test generation from state based use case models

We present a strategy for the automatic generation of test cases from parametrised use case templates that capture control flow, state, input and output. Our approach allows test scenario selection based on particular traces or states of the model. The templates are internally represented as CSP processes with explicit input and output alphabets, and test generation is expressed as counter-examples of refinement checking, mechanised using the FDR tool. Soundness is addressed through an input–output conformance relation formally defined in the CSP traces model. This purely process algebraic characterisation of testing has some potential advantages, mainly an easy automation of conformance verification and test case generation via model checking, without the need to develop any explicit algorithm.     

基于Linux环境的TCP协议一致性测试实现

依照的定义,阐述了协议一致性测试的基本概念、基本模型、测试方法、测试流程、测试描述语言。通过对系统ISO9646LinuxTCP协议的重新配置,利用系统提供的原始套接口和链路套接口,从而确保测试报文按照测试的要求发送和接Linuxsock_raw ()sock_packet() 收,最终简洁且高效地实现对复杂的协议的一致性测试。TCP     

Combining formal verification and conformance testing for validating reactive systems

This paper presents a combination of verification and conformance testing techniques to support the formal validation of reactive systems. The idea is to use symbolic test selection techniques to extract subgraphs (components) from a specification, and to perform the verification on the components rather than on the whole specification. Under reasonable sufficient conditions, this constitutes a sound compositional verification technique, in the sense that a property verified on the components also holds on the whole specification. This may considerably reduce the global verification effort. Moreover, once verified, a component forms the basis of an adequate test case, i.e. when executed on an implementation, it will not issue false positive or negative verdicts with respect to the verified properties. The approach has been implemented using the STG test selection tool and the PVS theorem prover. It is demonstrated here on a smart‐card application: the Common Electronic Purse System. Copyright © 2003 John Wiley & Sons, Ltd.     

WIA-PA无线通信一致性测试平台研究

分析了WIA-PA通信协议及其一致性测试,根据WIA-PA通信协议设计了WIA-PA无线通信一致性测试平台,并通过一个测试用例详细阐述了正向测试和反向测试的过程。实际测试结果表明,该测试平台能检测出设备是否符合WIA-PA标准协议,为WIA-PA设备在实际工业现场中的应用提供了可靠的保证。     

基于Tcl的BGP一致性测试系统设计

针对协议一致性测试的特点和要求，介绍了一种基于Tcl的BGP协议一致性测试系统的设计方法。相对于目前使用较多的基于TICN的方法，该方法具有灵活性高，模块独立性好等优点。文中给出了一个基于该系统的测试例的实例。初步实验结果表明该系统有较好的测试能力，为利用Tcl开发其它协议测试系统提供了有益借鉴。     

Formal firewall conformance testing: an application of test and proof techniques

Firewalls are an important means to secure critical ICT infrastructures. As configurable off‐the‐shelf products, the effectiveness of a firewall crucially depends on both the correctness of the implementation itself as well as the correct configuration. While testing the implementation can be done once by the manufacturer, the configuration needs to be tested for each application individually. This is particularly challenging as the configuration, implementing a firewall policy, is inherently complex, hard to understand, administrated by different stakeholders and thus difficult to validate. This paper presents a formal model of both stateless and stateful firewalls (packet filters), including NAT , to which a specification‐based conformance test case generation approach is applied. Furthermore, a verified optimisation technique for this approach is presented: starting from a formal model for stateless firewalls, a collection of semantics‐preserving policy transformation rules and an algorithm that optimizes the specification with respect of the number of test cases required for path coverage of the model are derived. We extend an existing approach that integrates verification and testing, that is, tests and proofs to support conformance testing of network policies. The presented approach is supported by a test framework that allows to test actual firewalls using the test cases generated on the basis of the formal model. Finally, a report on several larger case studies is presented. Copyright © 2014 John Wiley & Sons, Ltd.     

基于一致性测试理论的Statechart描述的测试用例自动生成

本文研究Statechart描述的测试语义和测试用例的自动生成.基于Tretmans的从标记转换系统描述自动生成测试用例的方法,我们研究如何从Statechart描述自动生成测试用例.本文的主要贡献在于建立了基于Statechart描述的一致性测试和测试用例生成的形式化基础.为Statechart描述建立了形式化测试语...     

基于Artifact快照序列的行为一致性检测方法

Artifact行为的一致性检测,是在流程建模、运行之后亟待解决的关键问题之一.针对现有一致性检测技术忽略数据操作方面检测的问题,提出了一种基于Artifact快照序列的行为一致性检测方法.首先,利用全序Artifact快照序列定义了Artifact的行为模式,该行为模式不仅体现了服务的运行轨迹,也描述出了Artifact数据属性赋值的状态变化;然后,将Artifact行为一致性检测问题转换为语言可判定问题,证明了该问题是一个可判定问题,该过程中,设计一台判定该语言的图灵机作为一致性验证模型,该模型不仅检测了Artifact生命周期中服务路径的一致性,同时也检测了生命周期中Artifact属性赋值的正确性;进一步地,利用服务-快照关联矩阵的等价转换,给出了行为一致性量化指标中确切度的精确计算方法;最后,通过实例分析及实验对所提出的方法进行了验证.     

AUTOSAR标准一致性测试研究

分析AUTOSAR一致性测试过程,采用eclipse、TTthree、μTTman等工具,基于TTCN-3测试系统架构,实现AUTOSAR一致性测试。针对简单信号灯系统,研究测试系统中测试套、编解码器和适配器的功能及相关实现方法,并验证采用TTCN-3进行AUTOSAR一致性测试的可行性。     

Validation of SDL specifications using EFSM-based test generation

Existing methods for testing an SDL specification mainly allow for either black box simulation or conformance testing to verify that the behavior of an implementation matches its corresponding model. However, this relies on the potentially hazardous assumption that the model is completely correct. We propose a test generation method that can accomplish conformance verification as well as coverage criteria-driven white box testing of the specification itself. We first reformat a set of EFSMs equivalent to the processes in an SDL specification and identify “hot spots” – nodes or edges in the EFSM which should be prioritized during testing to effectively increase coverage. Then, we generate test sequences intended to cover selected hot spots; we address the possible infeasibility of such a test sequence by allowing for its rejection decided by a constraint solver and re-generation of an alternate test sequence to the hot spot. In this paper, we present our test generation method and tool, and provide case studies on five SDL processes demonstrating the effectiveness of our coverage-based test sequence selection.     

WIA-PA协议一致性测试方法研究

针对WIA-PA协议的特点构建了WIA-PA协议一致性测试的系统结构和网络拓扑,给出了WIA-PA协议一致性测试的方法和原则,重点论述了测试代理软件的功能与软件实现,设计出了WIA-PA协议的一致性测试抽象测试集。最后以数据链路层的网络时间同步测试为例说明了WIA-PA协议一致性测试的一般流程。     

一种形式化的基于TTCN的测试执行方法

探讨基于形式化技术的测试执行方法是开展形式化的协议一致性测试活动的关键环节．本文提出了一种形式化的基于测试描述语言ＴＴＣＮ的操作语义的测试执行方法，并使用标号变迁系统刻画了这一方法的整个执行过程，同时讨论了这个方法的一个具体实现．这种形式化的基于ＴＴＣＮ的测试执行方法非常适合于构造通用的协议测试系统，同时也是进行测试集的自动验证的有效手段.     

Mechanical Verification of an Ideal Incremental ABR Conformance Algorithm

The Available Bit Rate protocol (ABR) for ATM networks is well adapted to data traffic by providing minimum rate guarantees and low cell loss to the ABR source end system. An ABR conformance algorithm for controlling the source rates through an interface has been defined by ATM Forum, and a more efficient version of it has been designed by Rabadan and Klay. We present in this work the first complete mechanical verification of the equivalence between these two algorithms. The proof is involved and has been supported by the PVS theorem prover. It has required many lemmas, case analysis, and induction reasoning for the manipulation of unbounded scheduling lists. Some ABR conformance protocols have been verified in previous works. However, these protocols are approximations of the one we consider here. In particular, the algorithms assume a bound on the number of rates to be scheduled.     

协议一致性测试执行系统的体系结构研究

对现有的协议一致性测试方法进行了介绍，然后针对TCP/IP协议族的一致性测试所必需的特殊要求和必需用到的多种测试方法，提出一种测试执行系统的体系结构，可以灵活地进行各个层次协议的测试。应用该体系结构开发的协议一致性测试套已经应用于高端路由器的研发中，为协议的顺利开发起到了积极的促进作用。     

管网SCADA系统通信协议一致性测试方法研究

针对油气管道SCADA系统的数据采集通信子系统支持协议种类较多的特点,文中提出一种基于虚拟仪器技术的协议一致性测试方法。针对不同通信协议调用不同的协议解析模块,但调用统一的一致性测试判定模块、测试结果输出分析模块,在测试判定模块中比较实测结果是否与根据标准协议得出的预期结果一致,进行一致性判定,最后利用Lab—VIEW软件平台实现了SCADA系统的调度中心、场站控制系统和现场设备的通信协议一致性测试。通过仿真和实验,验证了该方法的可行性和有效性。     

An approach to concurrent TTCN test generation

The basis of distributed system conformance testing is to test the conformance of each entity with its standard.This paper addresses the approach to entity conformance testing based on concurrent TTCN.First a preliminary framework for entity conformance testing is introduced and a specification model CEBE is presented.Then a test generation method,which could directly derive concurrent TTCN test suite from CEBE,is proposed.     

网络协议测试的符号化一致性关系研究

协议的一致性测试可以验证协议实现的正确性,一致性关系是测试生成的基础。网络协议的特点之一是控制消息中会携带大量数据。针对网络协议的该特点提出了符号化的一致性关系模型。建立了网络协议的输入输出符号变迁系统,并且依据数据符号实例化策略建立了对应的语义模型,在该模型中系统的活动是集成控制和数据的复杂活动。在此输入输出符号变迁模型的基础上提出了一种符号化的一致性关系以生成测试套。为了便于测试套的自动生成,对所提出的一致性关系进行了简化。在上述过程中数据的处理通过符号化的变量进行建模,这样可以使用统一符号进行数据处理,而不必总是关心具体的数值,只需在适当的时机进行符号的实例化。文中所提出的一致性关系模型充分利用了符号化的变量,增加了该模型的抽象程度,避免了处理过程的复杂性,且可以指导测试套的自动生成。最后使用IPv6的邻居发现协议对该一致性关系进行了说明。     

6LoWPAN协议一致性测试方法及仪表设计

针对6LoWPAN协议栈的MAC层、适配层、网络层及路由协议,研究6LoWPAN协议的一致性测试方法,将TTCN-3测试标准引入到无线传感器网络协议的一致性测试领域,设计了一套以TTCN-3为协议测试描述语言、以ISO9646中定义的协议一致性测试模型为方法的6LoWPAN协议一致性测试仪表.     

Improving active Mealy machine learning for protocol conformance testing

Using a well-known industrial case study from the verification literature, the bounded retransmission protocol, we show how active learning can be used to establish the correctness of protocol implementation I relative to a given reference implementation R. Using active learning, we learn a model M _R of reference implementation R, which serves as input for a model-based testing tool that checks conformance of implementation I to M _R . In addition, we also explore an alternative approach in which we learn a model M _I of implementation I, which is compared to model M _R using an equivalence checker. Our work uses a unique combination of software tools for model construction (Uppaal), active learning (LearnLib, Tomte), model-based testing (JTorX, TorXakis) and verification (CADP, MRMC). We show how these tools can be used for learning models of and revealing errors in implementations, present the new notion of a conformance oracle, and demonstrate how conformance oracles can be used to speed up conformance checking.