A compositional approach for modeling and timing analysis of wireless sensor and actuator networks
Abstract
Wireless sensor and actuator networks (WSAN) are created through the integration of multiple nodes which acquire data and perform reaction based on them. In a general overview, sensor nodes of WSANs are responsible for data acquisition and sending them to a central node. The central node stores all the received data and performs reactions. Timing verification of WSAN applications to ensure schedulability of tasks is a challenge, and is generally performed by worst-case analysis. This process is error-prone and inherently conservative. On the other hand, using model checking for analyzing WSAN applications results in state space explosion even for middle-sized configurations. The reason is the necessity of considering the interleaving of the large number of sensors in WSANs. In this paper, we show how to build an actor-based model of WSAN applications, starting from sensor node-level and moving towards the full system, and we show how this compositional modeling improves analysability and modifiability. Realtime extension of actor model is appropriate for modeling WSAN applications where we have many concurrent and asynchronous processes, and interdependent realtime deadlines. We demonstrate the approach using a case study of a distributed realtime data acquisition system for high-frequency sensing, where Timed Rebeca is used for modeling. We use model checking to check the intra/inter-sensor node schedulability.
References
[1]
Rebeca Formal Modeling Language. http://www.rebeca-lang.org/.
[2]
G. A. Agha. ACTORS - a model of concurrent computation in distributed systems. MIT Press series in artificial intelligence. MIT Press, 1990.
[3]
T. Amnell, E. Fersman, L. Mokrushin, P. Pettersson, and W. Yi. Times: A tool for schedulability analysis and code generation of real-time systems. In FORMATS, volume 2791 of Lecture Notes in Computer Science, pages 60--72. Springer, 2003.
[4]
E. M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999.
[5]
A. David, J. Illum, K. G. Larsen, and A. Skou. Model-Based Design for Embedded Systems, chapter Model-Based Framework for Schedulability Analysis Using UPPAAL 4.1, pages 93--119. CRC Press, 2010.
[6]
F. S. de Boer, T. Chothia, and M. M. Jaghoori. Modular Schedulability Analysis of Concurrent Objects in Creol. In Fundamentals of Software Engineering, Third IPM International Conference, FSEN 2009, Kish Island, Iran, April 15-17, 2009, Revised Selected Papers, volume 5961 of Lecture Notes in Computer Science, pages 212--227. Springer, 2009.
[7]
F. S. de Boer, M. M. Jaghoori, and E. B. Johnsen. Dating concurrent objects: Real-time modeling and schedulability analysis. In CONCUR, volume 6269 of Lecture Notes in Computer Science, pages 1--18. Springer, 2010.
[8]
A. El-Hoiydi. Spatial TDMA and CSMA with preamble sampling for low power ad hoc wireless sensor networks. In Proceedings of the Seventh IEEE Symposium on Computers and Communications (ISCC 2002), 1-4 July 2002, Taormina, Italy, pages 685--692. IEEE Computer Society, 2002.
[9]
E. Fersman, L. Mokrushin, P. Pettersson, and W. Yi. Schedulability Analysis of Fixed-Priority Systems Using Timed Automata. Theor. Comput. Sci., 354(2):301--317, 2006.
[10]
E. Fersman, P. Pettersson, and W. Yi. Timed automata with asynchronous processes: Schedulability and decidability. In TACAS, volume 2280 of Lecture Notes in Computer Science, pages 67--82. Springer, 2002.
[11]
J. Hill, R. Szewczyk, A. Woo, S. Hollar, D. Culler, and K. Pister. System architecture directions for networked sensors. SIGPLAN Notices, 35:93--104, November 2000.
[12]
Illinois SHM Services Toolsuite. http://shm.cs.illinois.edu/software.html.
[13]
A. Jafari, E. Khamespanah, M. Sirjani, H. Hermanns, and M. Cimini. Ptrebeca: Modeling and analysis of distributed and asynchronous systems. Sci. Comput. Program., 128:22--50, 2016.
[14]
E. Khamespanah, K. Mechitov, M. Sirjani, and G. A. Agha. Schedulability analysis of distributed real-time sensor network applications using actor-based model checking. In Model Checking Software - 23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, April 7-8, 2016, Proceedings, volume 9641 of Lecture Notes in Computer Science, pages 165--181. Springer, 2016.
[15]
E. Khamespanah, M. Sirjani, Z. Sabahi-Kaviani, R. Khosravi, and M. Izadi. Timed rebeca schedulability and deadlock freedom analysis using bounded floating time transition system. Sci. Comput. Program., 98:184--204, 2015.
[16]
E. Khamespanah, M. Sirjani, M. Viswanathan, and R. Khosravi. Floating Time Transition System: More Efficient Analysis of Timed Actors. In editors, Formal Aspects of Component Software - 12th International Symposium, FACS 2015, Rio de Janeiro, Brazil, October 14-16, 2015, Lecture Notes in Computer Science. Springer, 2016.
[17]
P. Levis, N. Lee, M. Welsh, and D. E. Culler. TOSSIM: accurate and scalable simulation of entire tinyos applications. In Proceedings of the 1st International Conference on Embedded Networked Sensor Systems, SenSys 2003, Los Angeles, California, USA, November 5-7, 2003, pages 126--137. ACM, 2003.
[18]
L. Linderman, K. Mechitov, and B. F. Spencer. TinyOS-Based Real-Time Wireless Data Acquisition Framework for Structural Health Monitoring and Control. Structural Control and Health Monitoring, 2012.
[19]
G. Lipari and G. Buttazzo. Schedulability analysis of periodic and aperiodic tasks with resource constraints. Journal of Systems Architecture, 46(4):327--338, 2000.
[20]
J. W. S. Liu. Real-Time Systems. Prentice Hall PTR, Upper Saddle River, NJ, USA, 1st edition, 2000.
[21]
C. Norström, A. Wall, and W. Yi. Timed automata as task models for event-driven systems. In RTCSA, pages 182--189. IEEE Computer Society, 1999.
[22]
P. C. Ölveczky and S. Thorvaldsen. Formal modeling, performance estimation, and model checking of wireless sensor network algorithms in real-time maude. Theor. Comput. Sci., 410(2-3):254--280, Feb. 2009.
[23]
J. Polastre, J. L. Hill, and D. E. Culler. Versatile low power media access for wireless sensor networks. In Stankovic et al. {30}, pages 95--107.
[24]
S. Ren and G. Agha. RTsynchronizer: Language Support for Real-Time Specifications in Distributed Systems. In Workshop on Languages, Compilers, & Tools for Real-Time Systems, pages 50--59. ACM, 1995.
[25]
A. H. Reynisson, M. Sirjani, L. Aceto, M. Cimini, A. Jafari, A. Ingólfsdóttir, and S. H. Sigurdarson. Modelling and Simulation of Asynchronous Real-Time Systems using Timed Rebeca. Sci. Comput. Program., 89:41--68, 2014.
[26]
Z. Sharifi, S. Mohammadi, and M. Sirjani. Comparison of NoC Routing Algorithms Using Formal Methods. To be published in proceedings of PDPTA'13, 2013.
[27]
Z. Sharifi, M. Mosaffa, S. Mohammadi, and M. Sirjani. Functional and performance analysis of network-on-chips using actor-based modeling and formal verification. ECEASST, 66, 2013.
[28]
V. Shnayder, M. Hempstead, B. Chen, G. Werner-Allen, and M. Welsh. Simulating the power consumption of large-scale sensor network applications. In Stankovic et al. {30}, pages 188--200.
[29]
B. F. Spencer Jr., H. Jo, K. Mechitov, J. Li, S.-H. Sim, R. Kim, S. Cho, L. Linderman, P. Moinzadeh, R. Giles, and G. Agha. Recent advances in wireless smart sensors for multi-scale monitoring and control of civil infrastructure. Journal of Civil Structural Health Monitoring, pages 1--25, 2015.
[30]
J. A. Stankovic, A. Arora, and R. Govindan, editors. Proceedings of the 2nd International Conference on Embedded Networked Sensor Systems, SenSys 2004, Baltimore, MD, USA, November 3-5, 2004. ACM, 2004.
[31]
S. Sundresh, W. Kim, and G. Agha. Sens: A sensor, environment and network simulator. In Proceedings 37th Annual Simulation Symposium (ANSS-37 2004), 18-22 April 2004, Arlington, VA, USA, pages 221--228. IEEE Computer Society, 2004.
- A compositional approach for modeling and timing analysis of wireless sensor and actuator networks
Recommendations
Modeling and analyzing real-time wireless sensor and actuator networks using actors and model checking
Programmers often use informal worst-case analysis and debugging to ensure that schedulers satisfy real-time requirements. Not only can this process be tedious and error-prone, it is inherently conservative and thus likely to lead to an inefficient use ...
Extending k-Coverage Lifetime of Wireless Sensor Networks Using Mobile Sensor Nodes
WIMOB '09: Proceedings of the 2009 IEEE International Conference on Wireless and Mobile Computing, Networking and CommunicationsOne of the important issues in wireless sensor network (WSN) is to k-cover the target sensing field and to extend its lifetime. We propose a method to k-cover the field and maximize the WSN lifetime by moving mobile sensor nodes to appropriate positions ...
Stream data gathering in wireless sensor networks within expected lifetime
MobiMedia '07: Proceedings of the 3rd international conference on Mobile multimedia communicationsSensor networks aim at collecting important sensor data for environment monitoring, e-health or hazardous conditions. Some applications do not need sensor networks with a long lifetime, such as monitoring an erupting volcano or monitoring hazardous ...
Comments
Information & Contributors
Information
Published In
October 2017
55 pages
Copyright © 2017 Authors.
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 22 November 2017
Published in SIGBED Volume 14, Issue 3
Check for updates
Author Tags
Qualifiers
- Research-article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 50Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 11 Feb 2025
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in