Topology-dependent Abstractions of Broadcast Networks | Sebastian Nanz, Flemming Nielson, Hanne Riis Nielson
| | 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. | | Type | Technical report | | Year | 2007 | | Publisher | Informatics and Mathematical Modelling, Technical University of Denmark, DTU | | Address | Richard Petersens Plads, Building 321, DK-2800 Kgs. Lyngby | | Series | IMM-Technical Report-2007-11 | | Electronic version(s) | [pdf] | | BibTeX data | [bibtex] | | IMM Group(s) | Computer Science & Engineering |
|