{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:56:23Z","timestamp":1750308983881,"version":"3.41.0"},"reference-count":31,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2017,11,22]],"date-time":"2017-11-22T00:00:00Z","timestamp":1511308800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGBED Rev."],"published-print":{"date-parts":[[2017,11,22]]},"abstract":"<jats:p>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.<\/jats:p>","DOI":"10.1145\/3166227.3166237","type":"journal-article","created":{"date-parts":[[2017,11,27]],"date-time":"2017-11-27T13:24:24Z","timestamp":1511789064000},"page":"49-56","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["A compositional approach for modeling and timing analysis of wireless sensor and actuator networks"],"prefix":"10.1145","volume":"14","author":[{"given":"Marjan","family":"Sirjani","sequence":"first","affiliation":[{"name":"Malardalen University, V\u00e4steras, Sweden and Reykjavik University, Reykjavik, Iceland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ehsan","family":"Khamespanah","sequence":"additional","affiliation":[{"name":"University of Tehran, Tehran, Iran and Reykjavik University, Reykjavik, Iceland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kirill","family":"Mechitov","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gul","family":"Agha","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2017,11,22]]},"reference":[{"unstructured":"Rebeca Formal Modeling Language. http:\/\/www.rebeca-lang.org\/.  Rebeca Formal Modeling Language. http:\/\/www.rebeca-lang.org\/.","key":"e_1_2_1_1_1"},{"key":"e_1_2_1_2_1","volume-title":"ACTORS - a model of concurrent computation in distributed systems","author":"Agha G. A.","year":"1990","unstructured":"G. A. Agha . ACTORS - a model of concurrent computation in distributed systems . MIT Press series in artificial intelligence. MIT Press , 1990 . G. A. Agha. ACTORS - a model of concurrent computation in distributed systems. MIT Press series in artificial intelligence. MIT Press, 1990."},{"key":"e_1_2_1_3_1","series-title":"Lecture Notes in Computer Science","first-page":"60","volume-title":"FORMATS","author":"Amnell T.","year":"2003","unstructured":"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 . 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."},{"key":"e_1_2_1_4_1","volume-title":"Model Checking","author":"Clarke E. M.","year":"1999","unstructured":"E. M. Clarke , O. Grumberg , and D. Peled . Model Checking . MIT Press , 1999 . E. M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999."},{"key":"e_1_2_1_5_1","first-page":"93","volume-title":"Model-Based Design for Embedded Systems","author":"David A.","year":"2010","unstructured":"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 . 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."},{"doi-asserted-by":"publisher","key":"e_1_2_1_6_1","DOI":"10.1007\/978-3-642-11623-0_12"},{"key":"e_1_2_1_7_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-642-17071-3","volume-title":"CONCUR","author":"de Boer F. S.","year":"2010","unstructured":"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 . 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."},{"doi-asserted-by":"publisher","key":"e_1_2_1_8_1","DOI":"10.5555\/839293.843207"},{"doi-asserted-by":"publisher","key":"e_1_2_1_9_1","DOI":"10.1016\/j.tcs.2005.11.019"},{"key":"e_1_2_1_10_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1007\/3-540-46002-0_6","volume-title":"TACAS","author":"Fersman E.","year":"2002","unstructured":"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 . 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."},{"doi-asserted-by":"publisher","key":"e_1_2_1_11_1","DOI":"10.1145\/356989.356998"},{"unstructured":"Illinois SHM Services Toolsuite. http:\/\/shm.cs.illinois.edu\/software.html.  Illinois SHM Services Toolsuite. http:\/\/shm.cs.illinois.edu\/software.html.","key":"e_1_2_1_12_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_13_1","DOI":"10.1016\/j.scico.2016.03.004"},{"key":"e_1_2_1_14_1","volume-title":"SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, April 7-8, 2016, Proceedings","volume":"9641","author":"Khamespanah E.","year":"2016","unstructured":"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 . 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."},{"doi-asserted-by":"publisher","key":"e_1_2_1_15_1","DOI":"10.1016\/j.scico.2014.07.005"},{"doi-asserted-by":"publisher","key":"e_1_2_1_16_1","DOI":"10.1007\/978-3-319-28934-2_13"},{"doi-asserted-by":"publisher","key":"e_1_2_1_17_1","DOI":"10.1145\/958491.958506"},{"key":"e_1_2_1_18_1","volume-title":"Structural Control and Health Monitoring","author":"Linderman L.","year":"2012","unstructured":"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 . 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."},{"doi-asserted-by":"publisher","key":"e_1_2_1_19_1","DOI":"10.1016\/S1383-7621(99)00009-0"},{"key":"e_1_2_1_20_1","volume-title":"Real-Time Systems","author":"Liu J. W. S.","year":"2000","unstructured":"J. W. S. Liu . Real-Time Systems . Prentice Hall PTR , Upper Saddle River, NJ, USA, 1 st edition, 2000 . J. W. S. Liu. Real-Time Systems. Prentice Hall PTR, Upper Saddle River, NJ, USA, 1st edition, 2000.","edition":"1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_21_1","DOI":"10.5555\/519167.828781"},{"doi-asserted-by":"publisher","key":"e_1_2_1_22_1","DOI":"10.1016\/j.tcs.2008.09.022"},{"doi-asserted-by":"publisher","key":"e_1_2_1_23_1","DOI":"10.1145\/1031495.1031508"},{"doi-asserted-by":"publisher","key":"e_1_2_1_24_1","DOI":"10.1145\/216636.216656"},{"doi-asserted-by":"publisher","key":"e_1_2_1_25_1","DOI":"10.1016\/j.scico.2014.01.008"},{"key":"e_1_2_1_26_1","volume-title":"Comparison of NoC Routing Algorithms Using Formal Methods. To be published in proceedings of PDPTA'13","author":"Sharifi Z.","year":"2013","unstructured":"Z. Sharifi , S. Mohammadi , and M. Sirjani . Comparison of NoC Routing Algorithms Using Formal Methods. To be published in proceedings of PDPTA'13 , 2013 . Z. Sharifi, S. Mohammadi, and M. Sirjani. Comparison of NoC Routing Algorithms Using Formal Methods. To be published in proceedings of PDPTA'13, 2013."},{"key":"e_1_2_1_27_1","first-page":"66","article-title":"Functional and performance analysis of network-on-chips using actor-based modeling and formal verification","author":"Sharifi Z.","year":"2013","unstructured":"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 . 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.","journal-title":"ECEASST"},{"doi-asserted-by":"publisher","key":"e_1_2_1_28_1","DOI":"10.1145\/1031495.1031518"},{"key":"e_1_2_1_29_1","first-page":"1","volume-title":"Journal of Civil Structural Health Monitoring","author":"Spencer B. F.","year":"2015","unstructured":"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 . 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."},{"key":"e_1_2_1_30_1","volume-title":"Proceedings of the 2nd International Conference on Embedded Networked Sensor Systems, SenSys 2004","author":"Stankovic J. A.","year":"2004","unstructured":"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. 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."},{"doi-asserted-by":"publisher","key":"e_1_2_1_31_1","DOI":"10.5555\/987679.987699"}],"container-title":["ACM SIGBED Review"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3166227.3166237","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3166227.3166237","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T21:41:06Z","timestamp":1750282866000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3166227.3166237"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,11,22]]},"references-count":31,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2017,11,22]]}},"alternative-id":["10.1145\/3166227.3166237"],"URL":"https:\/\/doi.org\/10.1145\/3166227.3166237","relation":{},"ISSN":["1551-3688"],"issn-type":[{"type":"electronic","value":"1551-3688"}],"subject":[],"published":{"date-parts":[[2017,11,22]]},"assertion":[{"value":"2017-11-22","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}