A systematic approach to constructing incremental topology control algorithms using graph transformation

https://doi.org/10.1016/j.jvlc.2016.10.003Get rights and content

Abstract

Communication networks form the backbone of our society. Topology control algorithms optimize the topology of such communication networks. Due to the importance of communication networks, a topology control algorithm should guarantee certain required consistency properties (e.g., connectivity of the topology), while achieving desired optimization properties (e.g., a bounded number of neighbors). Real-world topologies are dynamic (e.g., because nodes join, leave, or move within the network), which requires topology control algorithms to operate in an incremental way, i.e., based on the recently introduced modifications of a topology. Visual programming and specification languages are a proven means for specifying the structure as well as consistency and optimization properties of topologies. In this paper, we present a novel methodology, based on a visual graph transformation and graph constraint language, for developing incremental topology control algorithms that are guaranteed to fulfill a set of specified consistency and optimization constraints. More specifically, we model the possible modifications of a topology control algorithm and the environment using graph transformation rules, and we describe consistency and optimization properties using graph constraints. On this basis, we apply and extend a well-known constructive approach to derive refined graph transformation rules that preserve these graph constraints. We apply our methodology to re-engineer an established topology control algorithm, kTC, and evaluate it in a network simulation study to show the practical applicability of our approach.

Introduction

Topology control (TC) is an important research area in the wireless network communication domain. TC aims at adapting the topology of wireless networks to optimize, for instance, the total power consumption, while maintaining crucial constraints of the topology (e.g., connectivity) [1], [2], [3], [4], [5]. A TC algorithm typically works by (i) first selecting a subset of the links of the original topology so that all required constraints are fulfilled, and (ii) then adjusting the transmission power of each node to reach its farthest neighbor across one of these selected links. In realistic settings, context events such as movement of sensor nodes continuously modify the structure of a topology. Therefore, a TC algorithm should operate in an incremental way by efficiently updating only the affected subset of links based on the occurred context events.

The development of a TC algorithm is performed by highly skilled and experienced professionals. The development process usually starts with an informal specification of the basic properties of a TC algorithm. This informal description is then supplemented by a formal specification using a theoretically well-founded framework such as graph theory [6], [7], [8] or game theory [9], [10], which allows to prove that the algorithm preserves all required constraints. The first evaluation of a TC algorithm is typically carried out using a network simulator, which may be succeeded by a second evaluation in a testbed environment, i.e., on real wireless devices. Both types of evaluation require an implementation of the TC algorithm in one or—most often—two programming languages, such as Java or MATLAB for the simulation and C or C++ for the testbed evaluation [11]. This means that, in the end, the (hopefully) same TC algorithm is represented in two or three more or less completely different representations. In research publications, often only the formalization (along with the proofs of correctness and optimality) and a pseudo-code representation of the TC algorithm is given, while the implementations are typically omitted. Still, even for skilled researchers, it may be difficult to verify that the pseudo code is a valid implementation of the formal specification.

In the following, we illustrate this by means of the Cooperative Topology Control Algorithm (CTCA), proposed by Chu and Sethu in an IEEE INFOCOM paper in 2012 [12]. The authors first give a graph-based intuition of the proposed TC algorithm, which shall lead to an improved distribution of the nodes' lifetimes in a wireless sensor network [12], Section 3. The resulting goals are then formalized as so-called ordinary potential game [13], which allows to prove that the proposed algorithm eventually leads to a stable and optimal state of the network. The authors present an implementation of their algorithm in pseudo code, which is 83 lines long, distributed across four listings, and enriched with network-specific aspects such as communication message exchange; all these aspects make it highly non-trivial to understand the correspondences to the game-theoretic formalization [12], Section 5. In a simulation-based evaluation, the authors compare CTCA with other state-of-the-art TC algorithms. Unfortunately, no details about the simulation platform are given [12], Section 6. To the best of our knowledge, no testbed evaluation of CTCA has been performed yet.

While the previous example considers only one of the many existing TC algorithms, experience shows that it is (at least partly) representative. The example illustrates an obvious and prevalent gap between the formal specification, which serves for proving important properties of the algorithm, and the implementation, which serves for assessing the TC algorithm. Due to this gap, it inherently remains unclear whether the evaluated implementation of a TC algorithm fulfills the properties that have been proved based on the specification.

This is especially true for the case where an incrementally working TC algorithm is required. The transition from a batch TC algorithm, which takes a complete topology as input and produces a modified (optimized) complete topology as output, to an incremental version, which takes an arbitrary set of topology (context) modifications as input and produces a (minimal) set of topology adaptations as output, is an error-prone process. Experience shows that it is extremely challenging to cover all possible combinations of topology modifications in such a way that the computed topology adaptations never violate the given set of topology constraints and optimization goals. Contributions such as those by Zave show that even formalizations of well-known network algorithms often reveal special cases where these algorithms do not work properly [14], [15]. For a more comprehensive survey of the application of formal methods to networking algorithms, we refer the reader to [16].

Towards a seamless construction process for TC algorithms. It is the vision of our research activities as part of the collaborative research center MAKI (Multi-Mechanism Adaptation for the Future Internet1) to close the gap between a carefully crafted formal specification and its derived implementation as follows. We propose a methodology for constructing TC algorithms starting with a concise formal specification and refining this specification step-by-step to an efficiently working implementation. The resulting implementation is correct by construction if we can show that all refinement steps preserve the properties of the initial specification. For this purpose, we adhere to a model-driven engineering (MDE) [17] approach, which works as follows:

  • Topologies are formalized as models that are proper instances of a common meta-model that represents all relevant properties of the considered class of topologies, e.g., link-weighted topologies.

  • The meta-model of a studied topology class is extended with a set of consistency constraints and optimization goals.

  • Model transformation rules describe all relevant (context) modifications of a topology class and the expected constraint-preserving topology adaptations of the constructed TC algorithm.

  • Code generators translate the rule-based description of a TC algorithm into an efficiently working implementation that can be used in a software simulator or a hardware testbed for evaluation purposes.

Directed or undirected graphs are commonly used to formalize the structure of communication system topologies (e.g., [6], [7], [12], [18]) and TC algorithms are often sketched visually as sequences of topology graph modifications (e.g., [19], [20]). Therefore, graph transformation (GT) constitutes a natural basis for developing our MDE methodology. GT offers a set of rule-based and declarative techniques for the high-level specification of model- or graph-manipulating algorithms with a well-defined semantics [21], [22]. A variety of GT-based tools are available for formal specification and rapid prototyping purposes of specified algorithms [23], [24], [25], [26], [27], [28].

GT languages and tools are established representatives of the whole class of visual languages (VL). As a consequence, our selected approach adheres to the tradition of both the VL and the MDE community to adopt visual modeling and programming languages for the high-level description of the structure and behavior of communication systems and, more generally, of distributed information systems. Today, UML [29]—an assembly of a number of previously popular VLs (e.g., state charts, message sequence charts, ROOM structure diagrams)—is a well-established visual modeling language used for MDE activities in the area of communication and distributed systems (e.g., [30], [31], [32]). Languages like eMoflon [23] or MechatronicUML [33] even integrate GT concepts for dynamic communication topology manipulation purposes with UML-like activity, class, and composite structure diagrams as well as state charts. Apart from these languages, the VL community has already been developing visual programming languages with well-defined syntax and semantics for distributed communication and information system construction purposes for several decades (e.g., G-Net [34], [35]). A comprehensive survey of related research activities can be found in [36], [37], [38].

To summarize, the TC algorithm approach presented in this paper relies on the subclass of GT-based visual languages and follows the tradition of the formal program-construction-by-transformation approaches (see, e.g., [39]), which have their roots in research activities of the 1970s like the Munich project CIP (computer-aided intuition-guided programming) and are today part of the vision of model-driven engineering activities [40].

Model constraints may be used for specifying required or forbidden properties of models. Visual graph constraints have been introduced by the GT community as a means to characterize classes of graphs in a formal and declarative way [22], [41], [42]. For particular classes of graph constraints, formal refinement algorithms have been proposed that take a set of GT rules and graph constraints as input and produce a refined set of GT rules that preserve the given constraints [42], [41], [43]. More precisely, this means that applying the refined GT rules will not cause violations of the specified graph constraints.

A number of model-driven approaches for developing TC algorithms have been proposed (e.g., [44], [45], [32], [46], [47]) that target two major objectives: The first major objective is to reduce the complexity of developing TC algorithms from the point of view of domain experts by providing suitable (visual) abstractions, e.g., by using activity diagram-like syntax to specify the control flow of a TC algorithm. The second major objective is to simplify the testing and debugging by implementing the TC algorithm against a middleware layer, which enables that the exact same algorithm may be exercised inside a software simulation and a hardware testbed environment. However, to the best of our knowledge, none of these approaches focuses on integrating consistency properties constructively into the development process of TC algorithms. Instead, the proposed approaches focus on facilitating formal analysis, debugging, automated code generation, or the deployment of TC algorithms based on models.

Contribution. In this paper, we present a model-based methodology for constructing incremental TC algorithms that are guaranteed to preserve specified formal properties. More specifically, we eliminate the previously described gap between specification and implementation of TC algorithms as follows:

  • 1.

    We characterize the required and desired properties of output topologies of a TC algorithm using graph constraints (as described in [42]).

  • 2.

    We use GT rules to describe TC operations, which specify the possible modifications during an execution of a TC algorithm, and context events, which specify the possible modifications by the environment.

  • 3.

    We apply and enhance the constructive refinement approach for GT rules presented in [42], [43] to TC. Our approach is able to cope with temporarily constraint-violating rules, which contrary to [42], [43] may not be restricted.

  • 4.

    We exemplify our approach by constructing a representative TC algorithm, kTC [6], and assess it quantitatively in a network simulation environment.

This work is a considerable extension of [48]: First, we give a detailed explanation of our constructive approach; second, we show how the approach may be extended to cope with context events as well; and third, we evaluate our approach w.r.t. correctness, incrementality, performance, and general applicability.

Structure. The structure of this paper is illustrated in Fig. 1: Section 2 introduces the basic concepts of network topologies and topology control. Section 3 introduces graph constraints as a means to specify consistency properties of topologies as well as optimization goals of TC algorithms. Section 4 presents GT rules as a means to specify TC operations and context events. Section 5 describes the rule refinement procedure, which combines the GT rules of TC and context events with the graph constraints to produce refined GT rules that preserve the specified consistency properties of topologies and achieve the specified optimization goals. Section 6 presents the results of the evaluation, and Section 7 surveys related work. Section 8 concludes this paper with a summary and an outlook.

Section snippets

Network topologies and topology control

In this section, we introduce basic concepts of meta-modeling, wireless sensor networks and topology control, including the algorithm kTC [6], which serves as our running example.

Specifying consistent topologies using graph constraints

In this section, we characterize consistent and optimal output topologies of a TC algorithm by graph constraints. We begin with an introduction to the general concepts of graph patterns and graph constraints. Afterwards, we describe the concrete graph constraints that specify general structural consistency properties of topologies, general requirements of output topologies of TC algorithms in general, and the optimization goals of kTC in particular.

Specifying topology control and context event rules using graph transformation

In this section, we first present the basic concepts of graph transformation (GT) rules and programmed GT operations. Afterwards, we illustrate these concepts by specifying concrete TC and context event operations as GT rules and by specifying complete TC algorithms using programmed GT operations.

Refining topology control and context events rules to preserve graph constraints

The examples at the end of Section 4.3 clearly indicate that basic-tc, the template GT operation for developing kTC, enforces the unclassified-link constraint Cu, but fails to preserve even weak consistency. In this section, the TC and context event rules and the GT operation basic-tc are refined to achieve the following goals.

  • 1.

    The refined TC rules and context event rules preserve weak consistency.

  • 2.

    Each refined unrestrictable rule is applicable whenever its corresponding original rule is

Simulation-based evaluation

In this section, we evaluate the incremental specification of kTC constructed in Section 5. For this evaluation, we use the GT tool eMoflon [23] to automatically transform the specification of kTC into executable Java code. For simulating WSNs, we use the network simulation platform Simonstrator [61].

In Section 6.1, we present the research questions to be answered during this evaluation. In Section 6.2, we outline the evaluation setup. In 6.3 RQ1–correctness, 6.4 RQ2-incrementality, 6.6

Related work

In this section, we survey related work from the fields of modeling and checking consistency properties and formal methods as well as model-based software engineering in the communication network engineering domain.

Specifying, checking and enforcing consistency properties. Model checking [81] is an analysis technique used to verify particular properties of a system a posteriori, i.e., after a specification of the desired properties and an implementation of the regarded system has been

Conclusion

This section concludes the paper and highlights possible directions of future research.

Acknowledgements

This work has been funded by the German Research Foundation (DFG internal grant number 1053 (http://gepris.dfg.de/gepris/projekt/210487104)) as part of projects A01 and C01 within the Collaborative Research Center (CRC) 1053 – MAKI. The authors would like to thank Lukas Neumann for his considerable support during the creation of this paper.

References (119)

  • I. Schweizer, M. Wagner, D. Bradler, M. Mühlhauser, T. Strufe, kTC - Robust and Adaptive Wireless Ad-Hoc Topology...
  • R. Wattenhofer, A. Zollinger, XTC: A Practical Topology Control Algorithm for Ad-Hoc Networks, in: Proc. of Parallel...
  • N. Li et al.

    Design and analysis of an MST-based topology control algorithm

    IEEE Trans. Wirel. Commun.

    (2005)
  • H.-Y. Shi et al.

    Game theory for wireless sensor networks: a survey

    Sensors

    (2012)
  • G.Z. Papadopoulos et al.

    Performance evaluation methods in ad hoc and wireless sensor networks: a literature study

    IEEE Commun. Mag.

    (2016)
  • X. Chu, H. Sethu, Cooperative Topology Control with Adaptation for Improved Lifetime in Wireless Ad-Hoc Networks, in:...
  • P. Zave, Understanding SIP through Model-Checking, in: Principles, Systems and Applications of IP Telecommunications....
  • P. Zave

    Using lightweight modeling to understand chord

    SIGCOMM Comput. Commun. Rev.

    (2012)
  • J. Qadir et al.

    Applying formal methods to networking: theory, techniques, and applications

    IEEE Commun. Surv. Tutor.

    (2015)
  • M. Völter et al.

    Model-Driven Software Development: Technology, Engineering, Management

    (2013)
  • J. Blendin, J. Rückert, T. Volk, D. Hausheer, Adaptive Software Defined Multicast, in: Proc. of Network Softwarization...
  • R. Jacob, A. Richa, C. Scheideler, S. Schmid, H. Täubig, A Distributed Polylogarithmic Time Algorithm for...
  • S. Kniesburges et al.

    Re-chord: a self-stabilizing chord overlay network

    Theory Comput. Syst.

    (2014)
  • G. Rozenberg (Ed.), Handbook of Graph Grammars and Computing by Graph Transformation, vol. 1: Foundations, World...
  • H. Ehrig et al.

    Fundamentals of Algebraic Graph Transformation

    (2006)
  • E. Leblebici, A. Anjorin, A. Schürr, Developing eMoflon with eMoflon, in: Proc. of ICMT 2014, 138–145,...
  • A. Rensink, The GROOVE Simulator: A Tool for State Space Generation, in: Applications of Graph Transformations with...
  • T. Arendt, E. Biermann, S. Jurack, C. Krause, G. Taentzer, Henshin: Advanced Concepts and Tools for In-Place EMF Model...
  • R. Geiß, V. Batz, D. Grund, S. Hack, A.M. Szalkowski, GrGen: A Fast SPO-Based Graph Rewriting Tool, in: Proc. Intl....
  • G. Taentzer, AGG: A Tool Environment for Algebraic Graph Transformation, in: Proc. of AGTIVE'99, vol. 1779, Springer,...
  • U. Nickel, J. Niere, A. Zündorf, The FUJABA Environment, in: Proc. of ICSE, ACM, 742–745,...
  • O.M. Group, UML Specification, Version 2.0, OMG, URL 〈http://www.omg.org/spec/UML/〉,...
  • H. Gomaa, Designing Concurrent, Distributed, and Real-time Applications with UML, in: Proc. of the 23rd Intl....
  • H. Wada, P. Boonma, J. Suzuki, K. Oba, Modeling and Executing Adaptive Sensor Network Applications with the Matilda UML...
  • W. Schäfer, H. Wehrheim, Model-Driven Development with Mechatronic UML, in: Graph Transformations and Model-Driven...
  • T.-C. Chen et al.

    A simulator for distributed systems using g-nets

    Model. Simul.

    (1993)
  • K. Ng, J. Kramer, J. Magee, N. Dulay, A Visual Approach to Distributed Programming, in: Tools and Environments for...
  • K. Zhang

    Visual Languages and Applications

    (2007)
  • K. Marriott et al.

    Visual Language Theory

    (1998)
  • S.-K. K. Chang, E. Glinert, J.G. Bonar, M. Graf, A.T. Berztiss, Principles of Visual Programming Systems, Prentice Hall...
  • F. Bauer et al.

    Formal program construction by transformations-computer-aided, intuition-guided programming

    IEEE Trans. Softw. Eng.

    (1989)
  • R. France, B. Rumpe, Model-driven development of complex software: a research roadmap, in: Future of Software...
  • A. Habel, K.-H. Pennemann, Nested Constraints and Application Conditions for High-Level Structures, in: Formal Methods...
  • R. Heckel, A. Wagner, Ensuring Consistency of Conditional Graph Rewriting – A Constructive Approach, in: Proc. of Joint...
  • F. Deckwerth et al.

    Generating preconditions from graph constraints by higher order graph transformation

    ECEASST

    (2014)
  • C.-L. Fok et al.

    Agilla: a mobile agent middleware for self-adaptive wireless sensor networks

    ACM Trans. Auton. Adapt. Syst.

    (2009)
  • T. Rodrigues et al.

    An approach based on the domain perspective to develop WSAN applications

    Softw. Syst. Model.

    (2015)
  • K. Tei et al.

    Model-driven-development-based stepwise software development process for wireless sensor networks

    IEEE Trans. Syst. Man Cybern.

    (2015)
  • P. Baldwin, S. Kohli, E.A. Lee, X. Liu, Y. Zhao, Modeling of Sensor Nets in Ptolemy II, in: Proc. of the Intl....
  • R. Kluge, G. Varró, A. Schürr, A Methodology for Designing Dynamic Topology Control Algorithms via Graph...
  • Cited by (10)

    View all citing articles on Scopus
    View full text