Static analysis of topology-dependent broadcast networks

Sebastian Nanz, Flemming Nielson, Hanne Riis Nielson

    Research output: Contribution to journalJournal articleResearchpeer-review

    Abstract

    Broadcast semantics poses significant challenges over point-to-point communication when it comes to formal modelling and analysis. Current approaches to analysing broadcast networks have focused on fixed connectivities, but this is unsuitable in the case of wireless networks where the dynamically changing network topology is a crucial ingredient. In this paper, we develop a static analysis that automatically constructs an abstract transition system, labelled by actions and connectivity information, to yield a mobility-preserving finite abstraction of the behaviour of a network expressed in a process calculus with asynchronous local broadcast. Furthermore, we use model checking based on a 3-valued temporal logic to distinguish network behaviour which differs under changing connectivity patterns. (C) 2009 Elsevier Inc. All rights reserved.
    Original languageEnglish
    JournalInformation and Computation
    Volume208
    Issue number2
    Pages (from-to)117-139
    ISSN0890-5401
    DOIs
    Publication statusPublished - 2010

    Fingerprint Dive into the research topics of 'Static analysis of topology-dependent broadcast networks'. Together they form a unique fingerprint.

    Cite this