{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,21]],"date-time":"2025-11-21T22:37:27Z","timestamp":1763764647339,"version":"3.41.0"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319307336"},{"type":"electronic","value":"9783319307343"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-30734-3_25","type":"book-chapter","created":{"date-parts":[[2016,3,12]],"date-time":"2016-03-12T08:19:52Z","timestamp":1457770792000},"page":"373-392","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":28,"title":["On Time Actors"],"prefix":"10.1007","author":[{"given":"Marjan","family":"Sirjani","sequence":"first","affiliation":[]},{"given":"Ehsan","family":"Khamespanah","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,3,13]]},"reference":[{"key":"25_CR1","volume-title":"System Design, Modeling, and Simulation using Ptolemy II","author":"C Ptolemaeus","year":"2014","unstructured":"Ptolemaeus, C.: System Design, Modeling, and Simulation using Ptolemy II. Ptolemy.org, Berkeley (2014)"},{"issue":"4","key":"25_CR2","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":"10","key":"25_CR3","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":"25_CR4","unstructured":"Hewitt, C.: Description and Theoretical Analysis (Using Schemata) of PLANNER: A Language for Proving Theorems and Manipulating Models in a Robot. MIT Artificial Intelligence Technical Report 258, Department of Computer Science, MIT, April 1972"},{"key":"25_CR5","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":"25_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-642-24933-4_3","volume-title":"Formal Modeling: Actors, Open Systems, Biological Systems","author":"M Sirjani","year":"2011","unstructured":"Sirjani, M., Jaghoori, M.M.: Ten years of analyzing actors: Rebeca experience. In: Agha, G., Danvy, O., Meseguer, J. (eds.) Formal Modeling: Actors, Open Systems, Biological Systems. LNCS, vol. 7000, pp. 20\u201356. Springer, Heidelberg (2011)"},{"key":"25_CR7","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":"25_CR8","doi-asserted-by":"crossref","first-page":"1","DOI":"10.4204\/EPTCS.58.1","volume":"58","author":"Luca Aceto","year":"2011","unstructured":"Aceto, L., Cimini, M., Ing\u00f3lfsd\u00f3ttir, A., Reynisson, A.H., Sigurdarson, S.H., Sirjani, M.: Modelling and simulation of asynchronous real-time systems using timed Rebeca. In: Mousavi, M.R., Ravara, A. (eds.) FOCLASA. EPTCS, vol. 58, pp. 1\u201319 (2011)","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"25_CR9","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.: 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":"25_CR10","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-319-05416-2_12","volume-title":"Formal Techniques for Safety-Critical Systems","author":"Z Sabahi-Kaviani","year":"2014","unstructured":"Sabahi-Kaviani, Z., Khosravi, R., Sirjani, M., \u00d6lveczky, P.C., Khamespanah, E.: Formal semantics and analysis of timed Rebeca in real-time maude. In: Artho, C., \u00d6lveczky, P.C. (eds.) FTSCS 2013. CCIS, vol. 419, pp. 178\u2013194. Springer, Heidelberg (2014)"},{"key":"25_CR11","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 & Decentralized Control, AGERE! 2014, Portland, OR, USA, 20 October 2014, pp. 55\u201366. ACM (2014)","DOI":"10.1145\/2687357.2687366"},{"key":"25_CR12","unstructured":"Sharifi, Z., Mosaffa, M., Mohammadi, S., Sirjani, M.: Functional and performance analysis of network-on-chips using actor-based modeling and formal verification. ECEASST 66 (2013)"},{"key":"25_CR13","doi-asserted-by":"crossref","unstructured":"Mechitov, K.A., Khamespanah, E., Sirjani, M., Agha, G.: A model checking approach for schedulability analysis of distributed real-time sensor network applications. In: Submitted for Publication (2015)","DOI":"10.1007\/978-3-319-32582-8_11"},{"key":"25_CR14","unstructured":"Sharifi, Z., Mohammadi, S., Sirjani, M.: Comparison of NoC routing algorithms using formal methods. In: Proceedings of PDPTA 2013 (2013)"},{"issue":"6","key":"25_CR15","doi-asserted-by":"publisher","first-page":"572","DOI":"10.1109\/MDT.2008.167","volume":"25","author":"A Sheibanyrad","year":"2008","unstructured":"Sheibanyrad, A., Greiner, A., Panades, I.M.: Multisynchronous and fully asynchronous nocs for GALS architectures. IEEE Des. Test Comput. 25(6), 572\u2013580 (2008)","journal-title":"IEEE Des. Test Comput."},{"key":"25_CR16","doi-asserted-by":"crossref","unstructured":"Khamespanah, E., Sabahi-Kaviani, Z., Khosravi, R., Sirjani, M., Izadi, M.J.: Timed-Rebeca schedulability and deadlock-freedom analysis using floating-time transition system. In: Agha, G.A., Bordini, R.H., Marron, A., Ricci, A. (eds.) AGERE!@SPLASH, pp. 23\u201334. ACM (2012)","DOI":"10.1145\/2414639.2414645"},{"key":"25_CR17","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., et al. (eds.) FACS 2015. LNCS, vol. 9539, pp. 237\u2013255. Springer, Heidelberg (2016). doi:10.1007\/978-3-319-28934-2_13"},{"key":"25_CR18","unstructured":"Izadi, M.J.: An Actor Based Model for Modeling and Verification of Real-Time Systems. Master\u2019s thesis, University of Tehran, School of Electrical and Computer Engineering, Iran (2010)"},{"issue":"2","key":"25_CR19","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theoret. Comput. Sci. 126(2), 183\u2013235 (1994)","journal-title":"Theoret. Comput. Sci."},{"key":"25_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/BFb0020949","volume-title":"Hybrid Systems III","author":"J Bengtsson","year":"1996","unstructured":"Bengtsson, J., Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: UPPAAL - A tool suite for automatic verification of real-time systems. In: Alur, Rajeev, Sontag, Eduardo D., Henzinger, Thomas A. (eds.) HS 1995. LNCS, vol. 1066, pp. 232\u2013243. Springer, Heidelberg (1996)"},{"key":"25_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/11560548_14","volume-title":"Correct Hardware Design and Verification Methods","author":"L Lamport","year":"2005","unstructured":"Lamport, L.: Real-time model checking is really simple. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 162\u2013175. Springer, Heidelberg (2005)"},{"key":"25_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"485","DOI":"10.1007\/BFb0055643","volume-title":"CONCUR 1998 Concurrency Theory","author":"JE Bengtsson","year":"1998","unstructured":"Bengtsson, J.E., Jonsson, B., Lilius, J., Yi, W.: Partial order reductions for timed systems. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 485\u2013500. Springer, Heidelberg (1998)"},{"key":"25_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1007\/3-540-48320-9_30","volume-title":"CONCUR 1999. Concurrency Theory","author":"M Minea","year":"1999","unstructured":"Minea, M.: Partial Order reduction for model checking of timed automata. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 431\u2013446. Springer, Heidelberg (1999)"},{"key":"25_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/978-3-540-75454-1_16","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"J H\u00e5kansson","year":"2007","unstructured":"H\u00e5kansson, J., Pettersson, P.: Partial order reduction for verification of real-time components. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 211\u2013226. Springer, Heidelberg (2007)"},{"issue":"1\u20132","key":"25_CR25","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/s10990-007-9001-5","volume":"20","author":"PC \u00d6lveczky","year":"2007","unstructured":"\u00d6lveczky, P.C., Meseguer, J.: Semantics and pragmatics of real-time maude. High. Order Symbolic Comput. 20(1\u20132), 161\u2013196 (2007)","journal-title":"High. Order Symbolic Comput."},{"key":"25_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/978-3-540-78800-3_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"PC \u00d6lveczky","year":"2008","unstructured":"\u00d6lveczky, P.C., Meseguer, J.: The real-time maude tool. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 332\u2013336. Springer, Heidelberg (2008)"},{"issue":"1","key":"25_CR27","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","volume":"96","author":"J Meseguer","year":"1992","unstructured":"Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoret. Comput. Sci. 96(1), 73\u2013155 (1992)","journal-title":"Theoret. Comput. Sci."},{"issue":"1\u20133","key":"25_CR28","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1016\/j.tcs.2005.11.020","volume":"353","author":"F Laroussinie","year":"2006","unstructured":"Laroussinie, F., Markey, N., Schnoebelen, P.: Efficient timed model checking for discrete-time systems. Theoret. Comput. Sci. 353(1\u20133), 249\u2013271 (2006)","journal-title":"Theoret. Comput. Sci."},{"key":"25_CR29","doi-asserted-by":"crossref","unstructured":"Mechitov, K., Khamespanah, E., Sirjani, M., Agha, G.: Schedulability Analysis of Distributed Real-Time Sensor Network Applications using Actor-Based Model Checking. Technical Report(2015)","DOI":"10.1007\/978-3-319-32582-8_11"},{"key":"25_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/978-3-319-25423-4_14","volume-title":"Formal Methods and Software Engineering","author":"CC Din","year":"2015","unstructured":"Din, C.C., Tapia Tarifa, S.L., H\u00e4hnle, R., Johnsen, E.B.: History-based specification and verification of scalable concurrent and distributed systems. In: Butler, M., et al. (eds.) ICFEM 2015. LNCS, vol. 9407, pp. 217\u2013233. Springer, Heidelberg (2015). doi:10.1007\/978-3-319-25423-4_14"},{"issue":"7","key":"25_CR31","doi-asserted-by":"publisher","first-page":"729","DOI":"10.1109\/71.877831","volume":"11","author":"G Chiu","year":"2000","unstructured":"Chiu, G.: The odd-even turn model for adaptive routing. IEEE Trans. Parallel Distrib. Syst. 11(7), 729\u2013738 (2000)","journal-title":"IEEE Trans. Parallel Distrib. Syst."},{"key":"25_CR32","doi-asserted-by":"publisher","first-page":"1007","DOI":"10.1002\/stc.1514","volume":"20","author":"L Linderman","year":"2012","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. 20, 1007\u20131020 (2012)","journal-title":"Struct. Control Health Monit."},{"key":"25_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/3-540-54233-7_136","volume-title":"Automata, Languages and Programming","author":"W Yi","year":"1991","unstructured":"Yi, W.: CCS + time = an interleaving model for real time systems. In: Albert, J.L., Monien, B., Rodr\u00edguez-Artalejo, M. (eds.) Automata, Languages and Programming. LNCS, vol. 510, pp. 217\u2013228. Springer, Heidelberg (1991)"},{"key":"25_CR34","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, & Tools for Real-Time Systems, pp. 50\u201359. ACM (1995)","DOI":"10.1145\/216633.216656"},{"key":"25_CR35","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":"F de Boer","year":"2010","unstructured":"de Boer, F., 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":"25_CR36","unstructured":"Jaghoori, M.M., de Boer, F.S., Sirjani, M.: Task scheduling in Rebeca. In: NWPT, pp. 16\u201318 (2007)"},{"issue":"4","key":"25_CR37","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/s11761-013-0148-0","volume":"8","author":"E Albert","year":"2014","unstructured":"Albert, E., de Boer, F.S., H\u00e4hnle, R., Johnsen, E.B., Schlatte, R., Tarifa, S.L.T., Wong, P.Y.H.: Formal modeling and analysis of resource management for cloud architectures: an industrial case study using Real-Time ABS. Serv. Oriented Comput. Appl. 8(4), 323\u2013339 (2014)","journal-title":"Serv. Oriented Comput. Appl."},{"key":"25_CR38","unstructured":"Jafari, A., Khamespanah, E., Sirjani, M., Hermanns, H.: Performance analysis of distributed and asynchronous systems using probabilistic timed actors. ECEASST 70 (2014)"}],"container-title":["Lecture Notes in Computer Science","Theory and Practice of Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-30734-3_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T19:21:06Z","timestamp":1748805666000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-30734-3_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319307336","9783319307343"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-30734-3_25","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":"13 March 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}