TY - GEN
T1 - Redesign of the LMST wireless sensor protocol through formal modeling and statistical model checking
AU - Katelman, Michael
AU - Meseguer, José
AU - Hou, Jennifer
N1 - Copyright:
Copyright 2008 Elsevier B.V., All rights reserved.
PY - 2008
Y1 - 2008
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=46049089121&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=46049089121&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-68863-1_10
DO - 10.1007/978-3-540-68863-1_10
M3 - Conference contribution
AN - SCOPUS:46049089121
SN - 3540688625
SN - 9783540688624
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 150
EP - 169
BT - Formal Methods for Open Object-Based Distributed Systems - 10th IFIP WG 6.1 International Conference, FMOODS 2008, Proceedings
T2 - 10th IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS 2008
Y2 - 4 June 2008 through 6 June 2008
ER -