{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,4]],"date-time":"2026-06-04T08:55:20Z","timestamp":1780563320613,"version":"3.54.1"},"reference-count":38,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2017,11,20]],"date-time":"2017-11-20T00:00:00Z","timestamp":1511136000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2018,10]]},"DOI":"10.1007\/s10009-017-0480-3","type":"journal-article","created":{"date-parts":[[2017,11,20]],"date-time":"2017-11-20T15:16:49Z","timestamp":1511191009000},"page":"547-561","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Modeling and analyzing real-time wireless sensor and actuator networks using actors and model checking"],"prefix":"10.1007","volume":"20","author":[{"given":"Ehsan","family":"Khamespanah","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marjan","family":"Sirjani","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kirill","family":"Mechitov","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Gul","family":"Agha","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2017,11,20]]},"reference":[{"key":"480_CR1","series-title":"MIT Press Series in Artificial Intelligence","volume-title":"ACTORS\u2014A Model of Concurrent Computation in Distributed Systems","author":"GA Agha","year":"1990","unstructured":"Agha, G.A.: ACTORS\u2014A Model of Concurrent Computation in Distributed Systems. MIT Press Series in Artificial Intelligence. MIT Press, Cambridge (1990)"},{"key":"480_CR2","series-title":"Lecture Notes in Computer Science","first-page":"60","volume-title":"FORMATS","author":"T Amnell","year":"2003","unstructured":"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\u201372. Springer, Berlin (2003)"},{"key":"480_CR3","doi-asserted-by":"crossref","unstructured":"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\u201311 Dec 1996, IEEE Computer Society, pp. 153\u2013160 (1996)","DOI":"10.1145\/256562.256597"},{"key":"480_CR4","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"480_CR5","doi-asserted-by":"crossref","unstructured":"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\u2013119 (2010)","DOI":"10.1201\/9781420067859-c4"},{"key":"480_CR6","unstructured":"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\u201317 Apr 2009, Revised Selected Papers, vol. 5961 of Lecture Notes in Computer Science, Springer, pp. 212\u2013227 (2009)"},{"key":"480_CR7","doi-asserted-by":"crossref","unstructured":"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\u20134 July 2002, Taormina, Italy, pp. 685\u2013692, IEEE Computer Society (2002)","DOI":"10.1109\/ISCC.2002.1021748"},{"issue":"2","key":"480_CR8","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1016\/j.tcs.2005.11.019","volume":"354","author":"E Fersman","year":"2006","unstructured":"Fersman, E., Mokrushin, L., Pettersson, P., Yi, W.: Schedulability analysis of fixed-priority systems using timed automata. Theor. Comput. Sci. 354(2), 301\u2013317 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"480_CR9","doi-asserted-by":"crossref","unstructured":"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\u201382 (2002)","DOI":"10.1007\/3-540-46002-0_6"},{"key":"480_CR10","unstructured":"Hewitt, C., Bishop, P., Steiger, R.: A universal modular ACTOR formalism for artificial intelligence. In: Nilsson, N.J. (ed.) IJCAI, pp. 235\u2013245, William Kaufmann (1973)"},{"key":"480_CR11","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1145\/356989.356998","volume":"35","author":"J Hill","year":"2000","unstructured":"Hill, J., Szewczyk, R., Woo, A., Hollar, S., Culler, D., Pister, K.: System architecture directions for networked sensors. SIGPLAN Not. 35, 93\u2013104 (2000)","journal-title":"SIGPLAN Not."},{"key":"480_CR12","unstructured":"Illinois SHM Services Toolsuite. http:\/\/shm.cs.illinois.edu\/software.html"},{"key":"480_CR13","doi-asserted-by":"crossref","first-page":"22","DOI":"10.1016\/j.scico.2016.03.004","volume":"128","author":"A Jafari","year":"2016","unstructured":"Jafari, A., Khamespanah, E., Sirjani, M., Hermanns, H., Cimini, M.: Ptrebeca: modeling and analysis of distributed and asynchronous systems. Sci. Comput. Program. 128, 22\u201350 (2016)","journal-title":"Sci. Comput. Program."},{"issue":"5","key":"480_CR14","doi-asserted-by":"crossref","first-page":"402","DOI":"10.1016\/j.jlap.2009.02.009","volume":"78","author":"MM Jaghoori","year":"2009","unstructured":"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\u2013416 (2009)","journal-title":"J. Log. Algebr. Program."},{"key":"480_CR15","doi-asserted-by":"publisher","unstructured":"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\u2013378 (2017). https:\/\/doi.org\/10.1007\/s00236-015-0254-x","DOI":"10.1007\/s00236-015-0254-x"},{"key":"480_CR16","doi-asserted-by":"crossref","unstructured":"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\u201366, ACM (2014)","DOI":"10.1145\/2687357.2687366"},{"key":"480_CR17","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1016\/j.scico.2017.11.004"},{"key":"480_CR18","doi-asserted-by":"crossref","unstructured":"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\u201423rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, 7\u20138 Apr 2016, pp. 165\u2013181 (2016)","DOI":"10.1007\/978-3-319-32582-8_11"},{"key":"480_CR19","doi-asserted-by":"crossref","first-page":"184","DOI":"10.1016\/j.scico.2014.07.005","volume":"98","author":"E Khamespanah","year":"2015","unstructured":"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\u2013204 (2015)","journal-title":"Sci. Comput. Program."},{"key":"480_CR20","doi-asserted-by":"crossref","unstructured":"Khamespanah, E., Sirjani, M., Viswanathan, M., Khosravi, R.: Floating time transition system: more efficient analysis of timed actors. In: Braga, C., \u00d6lveczky, P.C. (eds.) Formal Aspects of Component Software\u201412th International Symposium, FACS 2015, Rio de Janeiro, Brazil, 14\u201316 oct 2015, Lecture Notes in Computer Science, Springer (2016)","DOI":"10.1007\/978-3-319-28934-2_13"},{"key":"480_CR21","doi-asserted-by":"crossref","unstructured":"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\u20137 Nov 2003, pp. 126\u2013137, ACM (2003)","DOI":"10.1145\/958491.958506"},{"key":"480_CR22","doi-asserted-by":"crossref","first-page":"1007","DOI":"10.1002\/stc.1514","volume":"20","author":"LE Linderman","year":"2012","unstructured":"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\u20131020 (2012)","journal-title":"Struct. Control Health Monit."},{"issue":"4","key":"480_CR23","doi-asserted-by":"crossref","first-page":"327","DOI":"10.1016\/S1383-7621(99)00009-0","volume":"46","author":"G Lipari","year":"2000","unstructured":"Lipari, G., Buttazzo, G.: Schedulability analysis of periodic and aperiodic tasks with resource constraints. J. Syst. Archit. 46(4), 327\u2013338 (2000)","journal-title":"J. Syst. Archit."},{"key":"480_CR24","volume-title":"Real-Time Systems","author":"JWS Liu","year":"2000","unstructured":"Liu, J.W.S.: Real-Time Systems, 1st edn. Prentice Hall, Upper Saddle River (2000)","edition":"1"},{"key":"480_CR25","doi-asserted-by":"crossref","unstructured":"Norstr\u00f6m, C., Wall, A., Yi, W.: Timed automata as task models for event-driven systems. In: RTCSA, IEEE Computer Society, pp. 182\u2013189 (1999)","DOI":"10.1109\/RTCSA.1999.811218"},{"issue":"2\u2014-3","key":"480_CR26","doi-asserted-by":"crossref","first-page":"254","DOI":"10.1016\/j.tcs.2008.09.022","volume":"410","author":"PC Olveczky","year":"2009","unstructured":"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\u2014-3), 254\u2013280 (2009)","journal-title":"Theor. Comput. Sci."},{"key":"480_CR27","doi-asserted-by":"publisher","unstructured":"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\u20135 Nov 2004, pp. 95\u2013107, ACM (2004). https:\/\/doi.org\/10.1145\/1031495.1031508","DOI":"10.1145\/1031495.1031508"},{"key":"480_CR28","first-page":"50","volume-title":"Workshop on Languages, Compilers, and Tools for Real-Time Systems","author":"S Ren","year":"1995","unstructured":"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\u201359. ACM, New York (1995)"},{"key":"480_CR29","unstructured":"Rebeca Formal Modeling Language. http:\/\/www.rebeca-lang.org\/"},{"key":"480_CR30","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1016\/j.scico.2014.01.008","volume":"89","author":"AH Reynisson","year":"2014","unstructured":"Reynisson, A.H., Sirjani, M., Aceto, L., Cimini, M., Jafari, A., Ing\u00f3lfsd\u00f3ttir, A., Sigurdarson, S.H.: Modelling and simulation of asynchronous real-time systems using timed Rebeca. Sci. Comput. Program. 89, 41\u201368 (2014)","journal-title":"Sci. Comput. Program."},{"key":"480_CR31","unstructured":"Zeinab, S., Mohammadi, S., Sirjani, M.: Comparison of NoC routing algorithms using formal methods. In: Proceedings of PDPTA\u201913 (2013)"},{"key":"480_CR32","unstructured":"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)"},{"key":"480_CR33","doi-asserted-by":"publisher","unstructured":"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\u20135 Nov 2004, pp. 188\u2013200, ACM (2004). https:\/\/doi.org\/10.1145\/1031495.1031518","DOI":"10.1145\/1031495.1031518"},{"issue":"10","key":"480_CR34","first-page":"1695","volume":"11","author":"M Sirjani","year":"2005","unstructured":"Sirjani, M., de Boer, F.S., Movaghar-Rahimabadi, A.: Modular verification of a component-based actor language. J. UCS 11(10), 1695\u20131717 (2005)","journal-title":"J. UCS"},{"key":"480_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1007\/978-3-642-24933-4_3","volume-title":"Formal Modeling: Actors, Open Systems, Biological Systems\u2014Essays Dedicated to Carolyn Talcott on the Occasion of Her 70th Birthday","author":"M Sirjani","year":"2011","unstructured":"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\u2014Essays Dedicated to Carolyn Talcott on the Occasion of Her 70th Birthday. Lecture Notes in Computer Science, vol. 7000, pp. 20\u201356. Springer, Berlin (2011)"},{"issue":"4","key":"480_CR36","doi-asserted-by":"crossref","first-page":"385","DOI":"10.3233\/FUN-2004-63405","volume":"63","author":"M Sirjani","year":"2004","unstructured":"Sirjani, M., Movaghar, A., Shali, A., de Boer, F.S.: Modeling and verification of reactive systems using Rebeca. Fundam. Inform. 63(4), 385\u2013410 (2004)","journal-title":"Fundam. Inform."},{"issue":"1","key":"480_CR37","first-page":"1","volume":"6","author":"BF Spencer","year":"2015","unstructured":"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\u201325 (2015)","journal-title":"J. Civ. Struct. Health Monit."},{"key":"480_CR38","unstructured":"Sameer, S., Kim, W.: et Gul Agha Sens: a sensor, environment and network simulator. In: Proceedings 37th Annual Simulation Symposium (ANSS-37 2004), 18\u201322 Apr 2004, Arlington, VA, USA, pp. 221\u2013228, IEEE Computer Society (2004)"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-017-0480-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-017-0480-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-017-0480-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,27]],"date-time":"2025-06-27T04:58:12Z","timestamp":1751000292000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-017-0480-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,11,20]]},"references-count":38,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2018,10]]}},"alternative-id":["480"],"URL":"https:\/\/doi.org\/10.1007\/s10009-017-0480-3","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,11,20]]}}}