Where academic tradition
meets the exciting future

Formal Development of Wireless Sensor–Actor Networks

Maryam Kamali, Linas Laibinis, Luigia Petre, Kaisa Sere, Formal Development of Wireless Sensor–Actor Networks. Science of Computer Programming 80 Part A, 25–49, 2014.

Abstract:

Wireless sensor–actor networks are a recent development of wireless networks where both ordinary sensor nodes and more sophisticated and powerful nodes, called actors, are present. In this paper we introduce several, increasingly more detailed, formal models for this type of wireless networks. These models formalise a recently introduced algorithm for recovering actor–actor coordination links via the existing sensor infrastructure. We prove via refinement that this recovery is correct and that it terminates in a finite number of steps. In addition, we propose a generalisation of our formal development strategy, which can be reused in the context of a wider class of networks. We elaborate our models within the Event-B formalism, while our proofs are carried out using the RODIN platform — an integrated development framework for Event-B.

BibTeX entry:

@ARTICLE{jKaLaPeSe14a,
  title = {Formal Development of Wireless Sensor–Actor Networks},
  author = {Kamali, Maryam and Laibinis, Linas and Petre, Luigia and Sere, Kaisa},
  journal = {Science of Computer Programming},
  volume = {80 Part A},
  publisher = {ELSEVIER},
  pages = {25–49},
  year = {2014},
  keywords = {Wireless sensor–actor networks (WSANs), Coordination links, Coordination recovery, Refinement, Pattern development, Event-B, Rodin},
}

Belongs to TUCS Research Unit(s): Distributed Systems Laboratory (DS Lab), Embedded Systems Laboratory (ESLAB)

Publication Forum rating of this publication: level 2

Edit publication