Redesign of the LMST wireless sensor protocol through formal modeling and statistical model checking

Michael Katelman, José Meseguer, Jennifer Hou

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

The local minimum spanning tree (LMST) topology control protocol tries to maintain connectivity in an ad-hoc wireless sensor network while minimizing power consumption and maximizing data bandwidth. Our formal, statistical model checking analysis of LMST under realistic deployment conditions shows that the invariant of maintaining network connectivity is easily lost. We then propose a formally-based system redesign methodology in which quantitative temporal logic formulas and further statistical model checking can be used to identify the causes of bugs, and to reach a correct system redesign. We show this methodology effective in the redesign of a version of LMST that ensures network connectivity under realistic deployment conditions.

Original languageEnglish (US)
Title of host publicationFormal Methods for Open Object-Based Distributed Systems - 10th IFIP WG 6.1 International Conference, FMOODS 2008, Proceedings
Pages150-169
Number of pages20
DOIs
StatePublished - 2008
Event10th IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS 2008 - Oslo, Norway
Duration: Jun 4 2008Jun 6 2008

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5051 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other10th IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS 2008
CountryNorway
CityOslo
Period6/4/086/6/08

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Redesign of the LMST wireless sensor protocol through formal modeling and statistical model checking'. Together they form a unique fingerprint.

Cite this