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 (7/13/20, 1:48 PM) Last edited by: TET group (7/13/20, 1:51 PM)
|Resource type: Thesis/Dissertation
ID no. (ISBN etc.): NNT: 2019SACL092
BibTeX citation key: Nguyen2019
View all bibliographic details
Keywords: model-based testing, test generation, Titan
Creators: Bannour, Prof. Le Gall, Nguyen
Publisher: Université Paris-Saclay (Paris)
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 , recommends analysing each of the traces in
an off-line mode up to the tioco conformance relation (using for example ) and the tuple of traces with
regard to some communication rules (using constraint solving techniques). Since the approach of , 
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, ,  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  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
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