TTCN-3 Bibliography
TTCN-3 Bibliography |
|
 |
 |
 |
|
Nguyen, N. M. T. (2019). test case generation for symbolic distributed system models: application to trickle based iot protocol. Unpublished Ph.D. Thesis, Université Paris-Saclay, Paris. Added by: TET group (13/07/2020, 13:48) Last edited by: TET group (13/07/2020, 13:51) |
| Resource type: Thesis/Dissertation ID no. (ISBN etc.): NNT: 2019SACL092 BibTeX citation key: Nguyen2019 View all bibliographic details  |
Categories: General Keywords: model-based testing, test generation, Titan Creators: Bannour, Prof. Le Gall, Nguyen Publisher: Université Paris-Saclay (Paris) Collection: |
Views: 77/1109
|
| Abstract |
|
Distributed systems (DS) consist of a number of independent subsystems, executing concurrently on different machines and interacting, by message passing, through a communication network so to complete a common objective. Such kind of systems are subjected to errors of different nature including errors related to excessive delays in replying to a received message or errors due to misplaced/erroneous data content for a received message. In order to capture, hence prevent the malicious effect of such errors, testing of DS becomes a vital pre-deployement task. Because of the peculiarities of DS (distributed nature, the lack of a global clock, non-deterministic behaviors), testing of DS turns out to be non trivial. In the context of testing distributed systems, this dissertation develops new insights by proposing a novel testing framework with regard to the issue of test data generation. The presented approach belongs to the family of Model-Based Testing approaches, i.e. those approaches where the specification of the System Under Test (SUT) and of what should be considered a correct implementation is formally described. We stress that our approach is not concerned with so-called oracle problem which consists of checking the traces to detect non-conformance between the SUT and the model using a mathematical conformance relation (for us tioco). Indeed, we have deliberately based our contribution in the context of the framework of distributed system modeling and testing described in [32, 10], which is very focused on the issue of conformance and its verification: in a few words, given a set of traces under the form of sequences of actions and durations, one per remote subsystem, the approach described in [32],[10] recommends analysing each of the traces in an off-line mode up to the tioco conformance relation (using for example [5]) and the tuple of traces with regard to some communication rules (using constraint solving techniques). Since the approach of [32], [10] has the advantage of being compositional and facilitating the resolution of the oracle problem, our modeling assumptions for distributed systems will be exactly the same. However, [32], [10] left aside the question of generating test data, whether in terms of managing test data or defining test selection criteria appropriate for DS.We therefore sought to complete the work of [10] with test generation capabilities, while keeping exactly the same test architecture, i.e. one test case per remote subsystem, to benefit from the same definitions and properties relating to conformance. In this context, in Chapter 2, we introduce the TIOSTS formalism that we have adopted for the purpose of modeling timed reactive systems. TIOSTS formalism makes it relatively easy to specify properties about data and time. Moreover the formalism has the key advantage of being equipped with symbolic execution 112 mechanisms. The main interest of this chapter is to set the main definitions and notations that will be used throughout the manuscript, to introduce small illustrative examples, to present the customizable Diversity platform allowing users to define their own functionalities about models and exploration strategies of their symbolic execution trees. In connection with the following chapters, the notion of deterministic models is precisely expressed in relation to properties of symbolic execution trees: this will be useful because it is expected that TIOSTS defining test cases are deterministic. For the same reasons, the facilities of the Diversity platform to target user-defined objectives are illustrated through a simple example, that of following a sequence of transitions from the initial model. In Chapter 3, we detail the construction of an online unitary test case, i.e. a test case with the ability to compute the next test data taking into account the previous reactions of the SUT. The main difficulty is to combine constraints on data and time, the possible occurrence of message arrivals on internal channels as well as the need to follow a test purpose defined as the form of a finite path of the symbolic execution tree. Let us recall here that the particularity of our approach for managing unitary test case design is to integrate that local systems SUT are tested in the context of a distributed system, i.e., in the context where third parties interact with the SUT through internal channels, without control on the part of the tester. The construction of the test case as a TIOSTS is defined using rules covering the different cases likely to occur depending on the progress in the test purpose, the reception on the internal channels, . . . Rules are in the form of a TIOSTS transition so that, by taking the test purpose as a guiding skeleton, it is possible to represent the test case as a rather particular TIOSTS (in the form of a tree with verdicts on the leaves). The implementation in Diversity is done in two steps, the first to build a symbolic execution tree of the reference model including the considered test objective, and the second to build transitions whose source nodes are those of the test purpose, by applying the rules. In Chapter 4, a distributed system is specified as a collection of unitary subsystems given as TIOSTS. System behaviors are captured by the symbolic execution of the whole system, defined by intertwining of symbolic executions of subsystems and modeling of asynchronous internal communications using waiting queues. Each symbolic path of the whole system defines by projection a family of local paths that can serve as local test purposes. The causality relation and the data identification are taken into account during the projection mechanism in order to provide local testers with these constraints that need to be satisfied by subsystems. As a part of our contribution, to provide the user with an alternative tool for the visualization of a global test purpose (besides the symbolic tree), we implemented in the Diversity tool a textual generator allowing for visualizing the global test purpose in the form of a sequence diagram annotated with temporal and data constraints reflecting the feasibility of the test purpose. In Chapter 5, we illustrate our testing method with a case study which is a Wireless Sensor Network based on the communication protocol MPL. The objective of the protocol is to update network nodes (i.e. devices) by means of the Trickle algorithm built for the MPL protocol. From the specification of the protocol, we constructed timed symbolic models. As part of our contribution, we implemented selection criteria in the Diversity tool that allow the generation of global test purposes which are relevant for testing from models. The interesting properties of the network that are expressed in a high level language, such as, e.g. all devices are updated or at least one device is outdated, can be considered as a global test purpose. With the aim of experimenting the selection criteria, their practical usage has been then highlighted by using the Diversity tool for generating different scenarios displaying up-to-date or outdated state of devices for many network topologies. |