Linking Simulation with Formal Verification and Modeling of Wireless Sensor Network in TLA

被引：2
作者：
Martyna, Jerzy [1 ]
机构：
[1] Jagiellonian Univ, Inst Comp Sci, PL-30348 Krakow, Poland
来源：
COMPUTER NETWORKS | 2010年 / 79卷
关键词：
SPIN protocol; flooding protocol; wireless sensor network; formal verification; TLA plus specification language; simulation;
D O I：
10.1007/978-3-642-13861-4_13
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
In this paper, we present the results of the simulation of a wireless sensor network based on the flooding technique and SPIN protocols. The wireless sensor network was specified and verified by means of the TLA+ specification language [1]. For a model of wireless sensor network built this way simulation was carried with the help of specially constructed software tools. The obtained results allow us to predict the behaviour of the wireless sensor network in various topologies and spatial densities. Visualization of the output data enable precise examination of some phenomenas in wireless sensor networks, such as a hidden terminal, etc.
引用
收藏
页码：131 / 140
页数：10
相关论文
共 24 条
[1]  
Abadi M., 1994, ACM T PROGR LANG SYS, V16, P166
[2]   Wireless sensor networks: a survey [J].
Akyildiz, IF ;
Su, W ;
Sankarasubramaniam, Y ;
Cayirci, E .
COMPUTER NETWORKS, 2002, 38 (04) :393-422
[3]  
Batson B, 2003, LECT NOTES COMPUT SC, V2852, P242
[4]   Design and evaluation of a wide-area event notification service [J].
Carzaniga, A ;
Rosenblum, DS ;
Wolf, AL .
ACM TRANSACTIONS ON COMPUTER SYSTEMS, 2001, 19 (03) :332-383
[5]  
Carzaniga A., 1999, THESIS POLITECNICO M
[6]  
Downey P., 2004, P 2004 INT C DEP SYS
[7]  
Glisic S.G., 2006, ADV WIRELESS NETWORK
[8]   On the use of IEEE 802.15.4 to enable wireless sensor networks in building automation [J].
Gutierrez, JA .
2004 IEEE 15TH INTERNATIONAL SYMPOSIUM ON PERSONAL, INDOOR AND MOBILE RADIO COMMUNICATIONS, VOLS 1-4, PROCEEDINGS, 2004, :1865-1869
[9]  
Heinzelman W. R., 1999, MobiCom'99. Proceedings of Fifth Annual ACM/IEEE International Conference on Mobile Computing and Networking, P174, DOI 10.1145/313451.313529
[10]  
Janowska A., 1998, VERIFICATION ESTELLE
123