Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Modeling and analyzing real-time wireless sensor and actuator networks using actors and model checking

  • SPIN 2016
  • Published:
International Journal on Software Tools for Technology Transfer Aims and scope Submit manuscript

Abstract

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 of resources. We propose to use model checking to find a schedule which optimizes the use of resources while satisfying real-time requirements. Specifically, we represent a Wireless sensor and actuator network (WSAN) as a collection of actors whose behaviors are specified using a Java-based actor language extended with operators for real-time scheduling and delay representation. We show how the abstraction mechanism and the compositionality of actors in the actor model may be used to incrementally build a model of a WSAN’s behavior from node-level and network models. We demonstrate the approach with a case study of a distributed real-time data acquisition system for high-frequency sensing using Timed Rebeca modeling language and the Afra model checking tool.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8

Similar content being viewed by others

Notes

  1. In this paper, we use rebec and actor interchangeably.

  2. The Timed Rebeca code of this case study, some complimentary shell scripts, the model checking toolset, and the details of the specifications of the state spaces in different configurations are accessible from the Rebeca homepage [29].

References

  1. Agha, G.A.: ACTORS—A Model of Concurrent Computation in Distributed Systems. MIT Press Series in Artificial Intelligence. MIT Press, Cambridge (1990)

    Google Scholar 

  2. Amnell, T., Fersman, E., Mokrushin, L., Pettersson, P., Yi, W.: Times: a tool for schedulability analysis and code generation of real-time systems. In: Larsen, K.M., Niebert, M.P. (eds.) FORMATS. Lecture Notes in Computer Science, pp. 60–72. Springer, Berlin (2003)

    Google Scholar 

  3. Buss, A.H.: Modeling with event graphs. In: Charnes, J.M., Morrice, D.J., Brunner, D.T., Swain, J.J. (eds.) Proceedings of the 28th Conference on Winter Simulation, WSC 1996, Coronado, CA, USA, 8–11 Dec 1996, IEEE Computer Society, pp. 153–160 (1996)

  4. Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)

    Google Scholar 

  5. David, A., Illum, J., Larsen, K.G., Skou, A.: Model-based design for embedded systems. In: Model-Based Framework for Schedulability Analysis Using UPPAAL 4.1, CRC Press, pp. 93–119 (2010)

  6. Frank, S., de Boer, F.S., Chothia, T., Jaghoori, M.M.: Modular schedulability analysis of concurrent objects in creol. In: Arbab, F., Sirjani, M. (eds.) Fundamentals of Software Engineering, Third IPM International Conference, FSEN 2009, Kish Island, Iran, 15–17 Apr 2009, Revised Selected Papers, vol. 5961 of Lecture Notes in Computer Science, Springer, pp. 212–227 (2009)

  7. El-Hoiydi, A.: 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, pp. 685–692, IEEE Computer Society (2002)

  8. Fersman, E., Mokrushin, L., Pettersson, P., Yi, W.: Schedulability analysis of fixed-priority systems using timed automata. Theor. Comput. Sci. 354(2), 301–317 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  9. Fersman, E., Pettersson, P., Yi, W.: Timed automata with asynchronous processes: schedulability and decidability. In: Katoen, J.P., Stevens, P. (eds.) TACAS, Lecture Notes in Computer Science, vol. 2280, Springer, pp. 67–82 (2002)

  10. Hewitt, C., Bishop, P., Steiger, R.: A universal modular ACTOR formalism for artificial intelligence. In: Nilsson, N.J. (ed.) IJCAI, pp. 235–245, William Kaufmann (1973)

  11. Hill, J., Szewczyk, R., Woo, A., Hollar, S., Culler, D., Pister, K.: System architecture directions for networked sensors. SIGPLAN Not. 35, 93–104 (2000)

    Article  Google Scholar 

  12. Illinois SHM Services Toolsuite. http://shm.cs.illinois.edu/software.html

  13. Jafari, A., Khamespanah, E., Sirjani, M., Hermanns, H., Cimini, M.: Ptrebeca: modeling and analysis of distributed and asynchronous systems. Sci. Comput. Program. 128, 22–50 (2016)

    Article  Google Scholar 

  14. Jaghoori, M.M., de Boer, F., Longuet, D., Chothia, T., Sirjani, M.: Schedulability of asynchronous real-time concurrent objects. J. Log. Algebr. Program. 78(5), 402–416 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  15. Jaghoori, M.M., de Boer, F.S., Longuet, D., Chothia, T., Sirjani, M.: Compositional schedulability analysis of real-time actor-based systems. Acta Inf. 54(4), 343–378 (2017). https://doi.org/10.1007/s00236-015-0254-x

  16. Khamespanah, E., Khosravi, R., Sirjani, M.: Efficient TCTL model checking algorithm for timed actors. In: Boix, E.G., Haller, P., Ricci, A., Varela, C. (eds.) Proceedings of the 4th International Workshop on Programming based on Actors Agents and Decentralized Control, AGERE! 2014, Portland, OR, USA, 20 Oct 2014, pp. 55–66, ACM (2014)

  17. Khamespanah, E., Khosravi, R., Sirjani, M.: An efficient TCTL model checking algorithm and a reduction technique for verification of timed actor models. Sci. Comput. Program. (2017)

  18. Khamespanah, E., Mechitov, K., Sirjani, M., Agha, G.: Schedulability analysis of distributed real-time sensor network applications using actor-based model checking. In: Proceedings of Model Checking Software—23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, 7–8 Apr 2016, pp. 165–181 (2016)

  19. Khamespanah, E., Sirjani, M., Sabahi-Kaviani, Z., Khosravi, R., Izadi, M.-J.: Timed rebeca schedulability and deadlock freedom analysis using bounded floating time transition system. Sci. Comput. Program. 98, 184–204 (2015)

    Article  Google Scholar 

  20. Khamespanah, E., Sirjani, M., Viswanathan, M., Khosravi, R.: Floating time transition system: more efficient analysis of timed actors. In: Braga, C., Ölveczky, P.C. (eds.) Formal Aspects of Component Software—12th International Symposium, FACS 2015, Rio de Janeiro, Brazil, 14–16 oct 2015, Lecture Notes in Computer Science, Springer (2016)

  21. Levis, P., Lee, N., Welsh, M., Culler, D.: TOSSIM: accurate and scalable simulation of entire tinyos applications. In: Akyildiz, I.E., Estrin, D., Culler, D.E., Srivastava, M.B. (eds.) Proceedings of the 1st International Conference on Embedded Networked Sensor Systems, SenSys 2003, Los Angeles, California, USA, 5–7 Nov 2003, pp. 126–137, ACM (2003)

  22. Linderman, L.E., Mechitov, K.A., Spencer, B.F.: TinyOS-based real-time wireless data acquisition framework for structural health monitoring and control. Struct. Control Health Monit. 20, 1007–1020 (2012)

    Article  Google Scholar 

  23. Lipari, G., Buttazzo, G.: Schedulability analysis of periodic and aperiodic tasks with resource constraints. J. Syst. Archit. 46(4), 327–338 (2000)

    Article  Google Scholar 

  24. Liu, J.W.S.: Real-Time Systems, 1st edn. Prentice Hall, Upper Saddle River (2000)

    Google Scholar 

  25. Norström, C., Wall, A., Yi, W.: Timed automata as task models for event-driven systems. In: RTCSA, IEEE Computer Society, pp. 182–189 (1999)

  26. Olveczky, P.C., Thorvaldsen, S.: Formal modeling, performance estimation, and model checking of wireless sensor network algorithms in real-time maude. Theor. Comput. Sci. 410(2—-3), 254–280 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  27. Polastre, J., Hill, J.L., Culler, D.E.: Versatile low power media access for wireless sensor networks. In: Stankovic, J.A., Arora, A., Govindan, R. (eds.) Proceedings of the 2nd International Conference on Embedded Networked Sensor Systems, SenSys 2004, Baltimore, MD, USA, 3–5 Nov 2004, pp. 95–107, ACM (2004). https://doi.org/10.1145/1031495.1031508

  28. Ren, S., Agha, G.: RTsynchronizer: language support for real-time specifications in distributed systems. In: Gerber, R., Marlowe, T.J. (eds.) Workshop on Languages, Compilers, and Tools for Real-Time Systems, pp. 50–59. ACM, New York (1995)

    Google Scholar 

  29. Rebeca Formal Modeling Language. http://www.rebeca-lang.org/

  30. Reynisson, A.H., Sirjani, M., Aceto, L., Cimini, M., Jafari, A., Ingólfsdóttir, A., Sigurdarson, S.H.: Modelling and simulation of asynchronous real-time systems using timed Rebeca. Sci. Comput. Program. 89, 41–68 (2014)

    Article  Google Scholar 

  31. Zeinab, S., Mohammadi, S., Sirjani, M.: Comparison of NoC routing algorithms using formal methods. In: Proceedings of PDPTA’13 (2013)

  32. Sharifi, Z., Mosaffa, M., Mohammadi, S., Sirjani, M.: Functional and performance analysis of network-on-chips using actor-based modeling and formal verification. In: ECEASST, vol. 66 (2013)

  33. Shnayder, V., Hempstead, M., Chen, B.R., Allen, G.W., Welsh, M.: Simulating the power consumption of large-scale sensor network applications. In: Stankovic, J.A., Arora, A., Govindan, R. (eds.) Proceedings of the 2nd International Conference on Embedded Networked Sensor Systems, SenSys 2004, Baltimore, MD, USA, 3–5 Nov 2004, pp. 188–200, ACM (2004). https://doi.org/10.1145/1031495.1031518

  34. Sirjani, M., de Boer, F.S., Movaghar-Rahimabadi, A.: Modular verification of a component-based actor language. J. UCS 11(10), 1695–1717 (2005)

    Google Scholar 

  35. Sirjani, M., Jaghoori, M.M.: Ten years of analyzing actors: Rebeca experience. In: Gul, A., Danvy, O., Meseguer, J. (eds.) Formal Modeling: Actors, Open Systems, Biological Systems—Essays Dedicated to Carolyn Talcott on the Occasion of Her 70th Birthday. Lecture Notes in Computer Science, vol. 7000, pp. 20–56. Springer, Berlin (2011)

    Chapter  Google Scholar 

  36. Sirjani, M., Movaghar, A., Shali, A., de Boer, F.S.: Modeling and verification of reactive systems using Rebeca. Fundam. Inform. 63(4), 385–410 (2004)

    MathSciNet  MATH  Google Scholar 

  37. Spencer, B.F., Jo, H., Mechitov, K.A., Li, J., Sim, S.H., Kim, R.E., Cho, S., Linderman, L.E., Moinzadeh, P., Giles, R.K., Agha, G.: Recent advances in wireless smart sensors for multi-scale monitoring and control of civil infrastructure. J. Civ. Struct. Health Monit. 6(1), 1–25 (2015)

    Google Scholar 

  38. Sameer, S., Kim, W.: et Gul Agha Sens: a sensor, environment and network simulator. In: Proceedings 37th Annual Simulation Symposium (ANSS-37 2004), 18–22 Apr 2004, Arlington, VA, USA, pp. 221–228, IEEE Computer Society (2004)

Download references

Acknowledgements

The work on this paper has been supported in part by the project “Self-Adaptive Actors: SEADA” (nr. 163205-051) of the Icelandic Research Fund, by Air Force Research Laboratory and the Air Force Office of Scientific Research under agreement number FA8750-11-2-0084, and by National Science Foundation under grant number CCF-1438982. The US Government is authorized to reproduce and distribute reprints for Governmental purposes notwithstanding any copyright notation thereon.

Author information

Authors and Affiliations

  1. School of ECE, University of Tehran, Tehran, Iran

    Ehsan Khamespanah

  2. School of Computer Science and CRESS, Reykjavik University, Reykjavík, Iceland

    Ehsan Khamespanah & Marjan Sirjani

  3. Mälardalen University, School of IDT, Västerås, Sweden

    Marjan Sirjani

  4. OSL, University of Illinois at Urbana-Champaign, Champaign, IL, USA

    Kirill Mechitov & Gul Agha

Authors
  1. Ehsan Khamespanah
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Marjan Sirjani
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Kirill Mechitov
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Gul Agha
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Ehsan Khamespanah.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Khamespanah, E., Sirjani, M., Mechitov, K. et al. Modeling and analyzing real-time wireless sensor and actuator networks using actors and model checking. Int J Softw Tools Technol Transfer 20, 547–561 (2018). https://doi.org/10.1007/s10009-017-0480-3

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10009-017-0480-3

Keywords

Search

Navigation