Special issue: Formal active and passive testing of distributed and networked systems

Vol. 70, n° 3-4, March-April 2015
Content available on Springerlink

Guest editors
Ana R. Cavalli, Télécom SudParis, France
Teruo Higashino, Osaka University, Japan
Manuel Núñez, Universidad Complutense de Madrid, Spain

Editorial

Ana R. Cavalli, Teruo Higashino, Manuel Núñez

A survey on formal active and passive testing with applications to the cloud

Ana R. Cavalli1, Teruo Higashino2, and Manuel Núñez3

(1) Télécom SudParis, France
(2) Osaka University, Japan
(3) Universidad Complutense de Madrid, Spain

Testing trust properties using a formal distributed network monitoring approach

Xiaoping Che1, 2, Jorge Lopez2, Stephane Maag2 and Gerardo Morales3

(1) Beijing Jiaotong University, People’s Republic of China
(2) Telecom SudParis, France
(3) Universidad Galileo, Guatemala, Guatemala

Abstract Collaborative systems are growing in use and in popularity. The need to boost the methods concerned by the interoperability is growing as well; making thus trustworthy interactions of the different systems a priority. The systems need to interact with users and with other applications in trusting each other. The decision regarding with who and how to interact with other users or applications depends on each application or system. In this paper, we focus on “soft trust”, that is trust management systems based on observations of the trustee behaviors to evaluate the trustee experience. Furthermore, we propose a formal distributed network monitoring approach to analyze the packets that the trustor and trustee exchange in order to prove the trustee is acting in a trustworthy manner. Based on formal “trust properties” defining the analyzed systems, the monitored systems behaviors on which these properties are checked provide, through testing verdicts, an evaluation of the trustor/trustee. Finally, our methodology is applied to a real industrial DNS use case scenario.

Keywords Trust systems – Network monitoring – Formal methods

Integration testing of communicating systems with unknown components

Roland Groz1, Keqin Li2 and Alexandre Petrenko3

(1) Université Grenoble Alpes, France
(2) SAP Product Security Research, Sophia Antipolis, France
(3) Computer Research Institute of Montreal (CRIM), Montreal, Quebec, Canada

Abstract The verification of a modular system composed of communicating components is a difficult problem, especially when the formal specifications, i.e. models of the components are not available. Conventional testing techniques are not efficient in detecting erroneous interactions of components because interleavings of internal events are difficult to reproduce in a modular asynchronous system. The problem of detecting intermittent errors and other compositional flaws in the absence of components’ models is addressed in this paper. A method for inferring a controllable approximation of communicating components through testing is elaborated. The inferred finite state models of components are used to detect compositional problems in the system through reachability analysis. To confirm a flaw in a particular component, a witness trace is used to construct a test applied to the component in isolation. The models are refined at each analysis step thus making the approach iterative. The proposed approach employs techniques for machine inference, testing and reachability analysis, and can reveal flaws due to the non-deterministic behaviour of a modular distributed system, such as unspecified receptions, livelocks, divergences, and races that would not be detected by testing alone. One key advantage of the approach is that by means of the inference parameter, it allows one to find a compromise between the co mplexity of testing the integrated system and the precision of the resulting models. The use of large tests is completely avoided in testing a component in isolation, since only single diagnostic test is executed in each iteration. Another advantage of the approach is that inferred models capture the functionalities of components used in the given system; unused behaviours of components are not modelled.

Keywords Model inference – Testing – Verification – Finite state machines – Intermittent errors

A methodology for validating cloud models using metamorphic testing

Alberto Núñez1, and Robert M. Hierons2

(1) Universidad Complutense de Madrid, Spain
(2) Brunel University, UK

Abstract Cloud computing is a paradigm that provides access to a flexible, elastic and on-demand computing infrastructure, allowing users to dynamically request virtual resources. However, researchers typically cannot experiment with critical parts of cloud systems such as the underlying cloud architecture, resource-provisioning policies and the configuration of resource virtualisation. This problem can be partially addressed through using simulations of cloud systems. Unfortunately, the problem of testing cloud systems is still challenging due to the many parameters that such systems typically have and the difficulty in determining whether an observed behaviour is correct. In order to alleviate these issues, we propose a methodology to semi-automatically test and validate cloud models by integrating simulation techniques and metamorphic testing.

Keywords Metamorphic testing – Cloud computing – Simulation and modelling

Class mutation operators for C++ object-oriented systems

Pedro Delgado-Pérez, Inmaculada Medina-Bulo, Juan José Domínguez-Jiménez, Antonio García-Domínguez and Francisco Palomo-Lozano

University of Cádiz, Spain

Abstract Mutation testing is a fault injection testing technique around which a great variety of studies and tools for different programming languages have been developed. Nevertheless, the mutation testing research with respect to C++ is pending. This paper proposes a set of class mutation operators related to this language and its particular object-oriented (OO) features. In addition, an implementation technique to apply mutation testing based on the traversal of the abstract syntax tree (AST) is presented. Finally, an experiment is conducted to study the operator behaviour with different C++ programs, suggesting their usefulness in the creation of complete test suites. The analysis includes a Web service (WS) library, one of the domains where this technique can prove useful, considering its challenging testing phase and that C++ is still a reference language for critical distributed systems WS.

Keywords Mutation testing – Mutation operators – C++ – Object-oriented programming – Abstract syntax tree – Web services

Open Topics

Tomofanout: a novel approach for large-scale IP traffic matrix estimation with excellent accuracy

Liansheng Tan and Haifeng Zhou

Central China Normal University, Wuhan, People’s Republic of China

Abstract Traffic matrix (TM) plays an important role in many network engineering and management tasks. However, the accurate TM estimation is still a challenge because the problem is highly under-constrained. In this paper, we propose a considerably accurate approach, termed as Tomofanout, for the estimation of TM in large-scale IP network using the available link load data, routing matrix, and partial direct measurement data of TM. Firstly, we propose an edge link fanout model which defines each edge link’s fanout, i.e., each edge link’s fractions of traffic emitting from that edge link to other edge links. Secondly, benefited from the edge link fanout’s diurnal pattern and stability, we are able to compute the edge link baseline fanout to estimate the TM at the following days by multiplying it by the edge link loads at the corresponding time intervals. In such way, an initial link-to-link TM estimation result is calculated by the edge link fanout model. Further, by making the corresponding transformation to the link-to-link TM, the router-to-router TM estimation result is thus obtained. Thirdly, the solution is then refined by the basic model of the Tomography method to keep consistent with both the edge and the interior link loads for further improvement of accuracy in estimation. In particular, the expectation maximization (EM) iteration of the basic model of Tomography method is used for further refinement. As the iteration is running on, the edge link fanout model solution is gradually approaching to the final estimation result, which is compatible with both the edge and the interior link loads. Fourthly, a general algorithm is proposed for computing the edge link baseline fanout and the estimation of the TM. Finally, the Tomofanout approach is validated by simulation studies using the real data from the Abilene Network. The simulation results demonstrate that Tomofanout achieves extremely high accuracy: its spatial relative error (SRE) is less than one half of Tomogravity’s, while its temporal relative error (TRE) is less than one half of Fanout’s and is only one third of Tomogravity’s.

Keywords Traffic matrix estimationTraffic engineeringNetwork capacity planning and managementNetwork optimizationSNMP

A cross-layer MAC and routing protocol based on slotted aloha for wireless sensor networks

David Espes1, Xavier Lagrange2 and Luis Suárez2

(1) University of Brest – LabSTICC, France
(2) Telecom-Bretagne – IRISA, Rennes, France

Abstract Wireless Sensor Networks (WSN) consist of a large number of sensors which have limited battery power. One of the major issues in WSN is the need to improve the overall network lifetime. Hence, WSN necessitate energy-efficient routing protocols. In this paper, a cross-layer routing protocol (PLOSA) is designed to offer a high delivery rate, a low end-to-end delay, and a low energy consumption. To achieve these goals, the transmission channel is divided into different slots, and a sensor has access to a slot related to its distance from the collector. The transmissions are then ordered within the frame from the farthest nodes to the closest ones which is a key point in order to ease forwarding and to conserve energy. We have conducted simulation-based evaluations to compare the performance of the proposed protocol against the framed aloha protocol. The performance results show that our protocol is a good candidate for WSN.

Keywords Sensor networks – Energy-awareness – Cross-layer protocol – Medium access control – Routing

Static hybrid multihop relaying and two hops hybrid relaying using DSTC

Sami Touati1, Hatem Boujemaa2, and Nazha Abed1

(1) King Saud University, Riyadh, Kingdom of Saudi Arabia
(2) University of Carthage, Ariana, Tunisia

Abstract In this paper, we propose a static hybrid multihop relaying protocol where some relays amplify the received signal whereas the remaining ones use decode and forward (DF) relaying. The relaying mode in each relay is set using the distance between the different nodes and the average SNR. The exact and asymptotic bit error probabilities, the block error probability and the throughput of hybrid automatic repeat request (HARQ) protocols are derived. Simulation results are provided in different contexts to compare the performance of hybrid relaying to conventional AF and DF relaying. In the second part of the paper, we propose a static hybrid amplify and forward (AF) and DF relaying using distributed space-time coding (DSTC). Relays close to the source amplify the received signal, and the remaining relays transmit only if they correctly decoded. All AF relays and DF relays that have correctly decoded transmit using DSTC in order to benefit from spatial diversity. The proposed protocol offers better performance than AF relaying using DSTC and similar performance to DF relaying using DSTC. However, the complexity and transmission delays of the proposed static hybrid AF-DF relaying is lower than that of DF relaying since decoding is not performed at AF relays.

Keywords Cooperative diversity – Decode and forward relaying – Amplify and forward relaying – DSTC – Rayleigh fading channels