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.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
Download to read the full chapter text
Chapter PDF
References
Agha, G., Gunter, C., Greenwald, M., Khanna, S., Meseguer, J., Sen, K., Thati, P.: Formal Modeling and Analysis of DoS Using Probabilistic Rewrite Theories. In: Foundations of Computer Security (FCS) (2005)
Agha, G., Meseguer, J., Sen, K.: PMaude: Rewrite-based Specification Language for Probabilistic Object Systems. In: Proc. of the Third Workshop on Quantitative Aspects of Programming Languages (QAPL 2005) (2005)
ANSI/IEEE. ANSI/IEEE Std 802.11, Edition (R2003) (1999)
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework. Springer, Heidelberg (2007)
Demaille, A., Hérault, T., Peyronnet, S.: Probabilistic Verification of Sensor Networks. In: Intl. Conf. on Research, Innovation and Vision for the Future (2006)
Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: HyTech: A Model Checker for Hybrid Systems. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 460–463. Springer, Heidelberg (1997)
Hérault, T., Lassaigne, R., Magniette, F., Peyronnet, S.: Approximate Probabilistic Model Checking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937. Springer, Heidelberg (2004)
Hermanns, H., Katoen, J.-P., Meyer-Kayser, J., Siegle, M.: A Markov Chain Model Checker. In: Schwartzbach, M.I., Graf, S. (eds.) ETAPS 2000 and TACAS 2000. LNCS, vol. 1785. Springer, Heidelberg (2000)
Jeannet, B., D’Argenio, P.R., Larsen, K.G.: Rapture: A tool for verifying Markov Decision Processes. In: Brim, L., Jančar, P., Křetínský, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol. 2421. Springer, Heidelberg (2002)
Katelman, M., Meseguer, J., Hou, J.: Formal Modeling, Analysis, and Debugging of a Localized Topology Control Protocol with Real-Time Maude and Probabilistic Model Checking. Technical report, University of Illinois at Urbana-Champaign (in preparation, 2008)
Kim, M., Stehr, M.-O., Talcott, C., Dutt, N., Venkatasubramanian, N.: A Probabilistic Formal Analysis Approach to Cross Layer Optimization in Distributed Embedded Systems. In: Bonsangue, M.M., Johnsen, E.B. (eds.) FMOODS 2007. LNCS, vol. 4468. Springer, Heidelberg (2007)
Kumar, N., Sen, K., Meseguer, J., Agha, G.: A Rewriting Based Model for Probabilistic Distributed Object Systems. In: Najm, E., Nestmann, U., Stevens, P. (eds.) FMOODS 2003. LNCS, vol. 2884. Springer, Heidelberg (2003)
Kwiatkowska, M., Norman, G., Parker, D.: Quantitative analysis with the probabilistic model checker PRISM. ENTCS 153(2), 5–31 (2005)
Kwiatkowska, M., Norman, G., Sproston, J.: Probabilistic Model Checking of the IEEE 802.11 Wireless Local Area Network Protocol. In: Proc. of the Second Joint Intl. Workshop on Process Algebra and Probabilistic Methods, Performance Modeling and Verification (PAPM-PROBMIV 2002) (2002)
Lamport, L.: Time, Clocks, and the Ordering of Events in a Distributed System. Communications of the ACM 21(7) (1978)
Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Intl. Journal on Software Tools for Technology Transfer 1(1-2), 134–152 (1997)
Li, N., Hou, J.C., Sha, L.: Design and Analysis of an MST-Based Topology Control Algorithm. In: INFOCOM 2003 (2003)
Meseguer, J.: Conditional Rewriting Logic as a Unified Model of Concurrency. Theor. Comput. Sci. 96(1), 73–155 (1992)
Meseguer, J., Sharykin, R.: Specification and Analysis of Distributed Object-Based Stochastic Hybrid Systems. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol. 3927, pp. 460–475. Springer, Heidelberg (2006)
Ölveczky, P.C., Meseguer, J.: Specification of Real-Time and Hybrid Systems in Rewriting Logic. Theoretical Computer Science 285, 359–405 (2002)
Ölveczky, P.C., Meseguer, J.: Semantics and pragmatics of Real-Time Maude. Higher Order and Symbolic Computation 20(1-2) (2007)
Ölveczky, P.C., Thorvaldsen, S.: Formal modeling and analysis of wireless sensor network algorithms in Real-Time Maude. In: 20th Intl. Parallel and Distributed Processing Symposium (IPDPS 2006) (2006)
Ölveczky, P.C., Thorvaldsen, S.: Formal Modeling and Analysis of the OGDC Wireless Sensor Network Algorithm in Real-Time Maude. In: Bonsangue, M.M., Johnsen, E.B. (eds.) FMOODS 2007. LNCS, vol. 4468. Springer, Heidelberg (2007)
Parzen, E.: Modern Probability Theory and Its Applications. John Wiley & Sons, Inc., Chichester (1960)
Sen, K., Viswanathan, M., Agha, G.: VESTA: A Statistical Model Checker and Analyzer for Probabilistic Systems. In: 2nd Intl. Conf. on the Quantitative Evaluation of Systems (2005)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Katelman, M., Meseguer, J., Hou, J. (2008). Redesign of the LMST Wireless Sensor Protocol through Formal Modeling and Statistical Model Checking. In: Barthe, G., de Boer, F.S. (eds) Formal Methods for Open Object-Based Distributed Systems. FMOODS 2008. Lecture Notes in Computer Science, vol 5051. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-68863-1_10
Download citation
DOI: https://doi.org/10.1007/978-3-540-68863-1_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-68862-4
Online ISBN: 978-3-540-68863-1
eBook Packages: Computer ScienceComputer Science (R0)