{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,2]],"date-time":"2025-06-02T07:40:09Z","timestamp":1748850009361,"version":"3.41.0"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319325811"},{"type":"electronic","value":"9783319325828"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-32582-8_11","type":"book-chapter","created":{"date-parts":[[2016,4,7]],"date-time":"2016-04-07T10:04:23Z","timestamp":1460023463000},"page":"165-181","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Schedulability Analysis of Distributed Real-Time Sensor Network Applications Using Actor-Based Model Checking"],"prefix":"10.1007","author":[{"given":"Ehsan","family":"Khamespanah","sequence":"first","affiliation":[]},{"given":"Kirill","family":"Mechitov","sequence":"additional","affiliation":[]},{"given":"Marjan","family":"Sirjani","sequence":"additional","affiliation":[]},{"given":"Gul","family":"Agha","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,4,8]]},"reference":[{"key":"11_CR1","unstructured":"Rebeca Formal Modeling Language. http:\/\/www.rebeca-lang.org\/"},{"key":"11_CR2","series-title":"MIT Press Series in Artificial Intelligence","volume-title":"ACTORS - A Model of Concurrent Computation in Distributed Systems","author":"GA Agha","year":"1990","unstructured":"Agha, G.A.: ACTORS - A Model of Concurrent Computation in Distributed Systems. MIT Press Series in Artificial Intelligence. MIT Press, Cambridge (1990)"},{"key":"11_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/978-3-540-40903-8_6","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"T Amnell","year":"2004","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.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol. 2791, pp. 60\u201372. Springer, Heidelberg (2004)"},{"key":"11_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":"11_CR5","first-page":"93","volume-title":"Model-Based Design for Embedded Systems","author":"A David","year":"2010","unstructured":"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\u2013119. CRC Press, Boca Raton (2010)"},{"key":"11_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/978-3-642-11623-0_12","volume-title":"Fundamentals of Software Engineering","author":"FS Boer de","year":"2010","unstructured":"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\u2013227. Springer, Heidelberg (2010)"},{"key":"11_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-15375-4_1","volume-title":"CONCUR 2010 - Concurrency Theory","author":"FS Boer de","year":"2010","unstructured":"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\u201318. Springer, Heidelberg (2010)"},{"key":"11_CR8","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":"11_CR9","doi-asserted-by":"publisher","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":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/3-540-46002-0_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Fersman","year":"2002","unstructured":"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\u201382. Springer, Heidelberg (2002)"},{"key":"11_CR11","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":"11_CR12","doi-asserted-by":"crossref","unstructured":"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\u2013104, November 2000","DOI":"10.1145\/356989.356998"},{"key":"11_CR13","unstructured":"Illinois SHM Services Toolsuite. http:\/\/shm.cs.illinois.edu\/software.html"},{"issue":"3","key":"11_CR14","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1109\/TII.2010.2051813","volume":"6","author":"MR Jongerden","year":"2010","unstructured":"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\u2013286 (2010)","journal-title":"IEEE Trans. Industr. Inf."},{"key":"11_CR15","doi-asserted-by":"publisher","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":"11_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/978-3-319-28934-2_13","volume-title":"Formal Aspects of Component Software","author":"E Khamespanah","year":"2016","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.) FACS 2015. LNCS, vol. 9539, pp. 237\u2013255. Springer, Heidelberg (2016)"},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"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\u20137 November 2003, pp. 126\u2013137. ACM (2003)","DOI":"10.1145\/958491.958506"},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1002\/stc.1514"},{"issue":"4","key":"11_CR19","doi-asserted-by":"publisher","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. Architect. 46(4), 327\u2013338 (2000)","journal-title":"J. Syst. Architect."},{"key":"11_CR20","volume-title":"Real-Time Systems","author":"JWS Liu","year":"2000","unstructured":"Liu, J.W.S.: Real-Time Systems, 1st edn. Prentice Hall PTR, Upper Saddle River (2000)","edition":"1"},{"key":"11_CR21","doi-asserted-by":"crossref","unstructured":"Norstr\u00f6m, C., Wall, A., Yi, W.: Timed automata as task models for event-driven systems. In: RTCSA, pp. 182\u2013189. IEEE Computer Society (1999)","DOI":"10.1109\/RTCSA.1999.811218"},{"issue":"2\u20133","key":"11_CR22","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1016\/j.tcs.2008.09.022","volume":"410","author":"PC \u00d6lveczky","year":"2009","unstructured":"\u00d6lveczky, 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\u20133), 254\u2013280 (2009)","journal-title":"Theor. Comput. Sci."},{"key":"11_CR23","unstructured":"Polastre, J., Hill, J.L., Culler, D.E.: Versatile low power media access for wireless sensor networks. In: Stankovic et al. [30], pp. 95\u2013107"},{"key":"11_CR24","doi-asserted-by":"crossref","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 (1995)","DOI":"10.1145\/216633.216656"},{"key":"11_CR25","doi-asserted-by":"publisher","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":"11_CR26","unstructured":"Sharifi, Z., Mohammadi, S., Sirjani, M.: Comparison of NoC routing algorithms using formal methods. In: Proceedings of PDPTA 2013 (2013, to be published)"},{"key":"11_CR27","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":"11_CR28","doi-asserted-by":"crossref","unstructured":"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\u2013200","DOI":"10.1145\/1031495.1031518"},{"key":"11_CR29","doi-asserted-by":"crossref","unstructured":"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\u201325 (2015)","DOI":"10.1007\/s13349-015-0111-1"},{"key":"11_CR30","unstructured":"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 November 2004. ACM (2004)"},{"key":"11_CR31","doi-asserted-by":"crossref","unstructured":"Sundresh, S., Kim, W.Y., Agha, G.: Sens: a sensor, environment and network simulator. In: Proceedings 37th Annual Simulation Symposium (ANSS-37 2004), 18\u201322 April 2004, Arlington, VA, USA, pp. 221\u2013228. IEEE Computer Society (2004)","DOI":"10.1109\/SIMSYM.2004.1299486"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-32582-8_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,2]],"date-time":"2025-06-02T07:05:41Z","timestamp":1748847941000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-32582-8_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319325811","9783319325828"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-32582-8_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"8 April 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}