nach oben

Erschienen in:

2016 | OriginalPaper | Buchkapitel

Schedulability Analysis of Distributed Real-Time Sensor Network Applications Using Actor-Based Model Checking

verfasst von : Ehsan Khamespanah, Kirill Mechitov, Marjan Sirjani, Gul Agha

Erschienen in: Model Checking Software

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Programmers often use informal worst-case analysis and debugging to ensure schedules that 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 behavior is specified using a C-based actor language extended with operators for real-time scheduling and delay representation. We show how the abstraction and compositionality properties of 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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Finite-Horizon Bisimulation Minimisation for Probabilistic Systems

Nächstes Kapitel smid: A Black-Box Program Driver

The TR 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 [1].

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

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

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.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol. 2791, pp. 60–72. Springer, Heidelberg (2004)CrossRef

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

David, A., Illum, J., Larsen, K.G., Skou, A.: Model-based framework for schedulability analysis using UPPAAL 4.1. In: Nicolescu, G., Mosterman, P.J. (eds.) Model-Based Design for Embedded Systems, pp. 93–119. CRC Press, Boca Raton (2010)

de Boer, F.S., Chothia, T., Jaghoori, M.M.: Modular schedulability analysis of concurrent objects in Creol. In: Arbab, F., Sirjani, M. (eds.) FSEN 2009. LNCS, vol. 5961, pp. 212–227. Springer, Heidelberg (2010)CrossRef

de Boer, F.S., Jaghoori, M.M., Johnsen, E.B.: Dating concurrent objects: real-time modeling and schedulability analysis. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 1–18. Springer, Heidelberg (2010)CrossRef

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)

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)MathSciNetCrossRefMATH

10.

Fersman, E., Pettersson, P., Yi, W.: Timed automata with asynchronous processes: schedulability and decidability. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 67–82. Springer, Heidelberg (2002)CrossRef

11.

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)

12.

Hill, J., Szewczyk, R., Woo, A., Hollar, S., Culler, D., Pister, K.: System architecture directions for networked sensors. In: SIGPLAN Notices, vol. 35, pp. 93–104, November 2000

13.

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

14.

Jongerden, M.R., Mereacre, A., Bohnenkamp, H.C., Haverkort, B.R., Katoen, J.-P.: Computing optimal schedules for battery usage in embedded systems. IEEE Trans. Industr. Inf. 6(3), 276–286 (2010)CrossRef

15.

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)CrossRef

16.

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.) FACS 2015. LNCS, vol. 9539, pp. 237–255. Springer, Heidelberg (2016)CrossRef

17.

Levis, P., Lee, N., Welsh, M., Culler, D.E.: TOSSIM: accurate and scalable simulation of entire tinyos applications. In Akyildiz, I.F., 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 November 2003, pp. 126–137. ACM (2003)

18.

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

19.

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

20.

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

21.

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

22.

Ölveczky, 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)MathSciNetCrossRefMATH

23.

Polastre, J., Hill, J.L., Culler, D.E.: Versatile low power media access for wireless sensor networks. In: Stankovic et al. [30], pp. 95–107

24.

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 (1995)

25.

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)CrossRef

26.

Sharifi, Z., Mohammadi, S., Sirjani, M.: Comparison of NoC routing algorithms using formal methods. In: Proceedings of PDPTA 2013 (2013, to be published)

27.

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)

28.

Shnayder, V., Hempstead, M., Chen, B.-R., Werner-Allen, G., Welsh, M.: Simulating the power consumption of large-scale sensor network applications. In: Stankovic et al. [30], pp. 188–200

29.

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

30.

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 November 2004. ACM (2004)

31.

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

Titel: Schedulability Analysis of Distributed Real-Time Sensor Network Applications Using Actor-Based Model Checking
verfasst von: Ehsan Khamespanah
Kirill Mechitov
Marjan Sirjani
Gul Agha
Verlag: Springer International Publishing
Buch: Model Checking Software
Print ISBN: 978-3-319-32581-1

Electronic ISBN: 978-3-319-32582-8

Copyright-Jahr: 2016
DOI: https://doi.org/10.1007/978-3-319-32582-8_11

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"