{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T10:52:44Z","timestamp":1761648764470},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2020,6,30]],"date-time":"2020-06-30T00:00:00Z","timestamp":1593475200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,6,30]],"date-time":"2020-06-30T00:00:00Z","timestamp":1593475200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/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":[[2020,10]]},"DOI":"10.1007\/s10009-020-00579-8","type":"journal-article","created":{"date-parts":[[2020,6,30]],"date-time":"2020-06-30T10:03:46Z","timestamp":1593511426000},"page":"617-633","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["VeriVANca framework: verification of VANETs by property-based message passing of actors in Rebeca with inheritance"],"prefix":"10.1007","volume":"22","author":[{"given":"Farnaz","family":"Yousefi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ehsan","family":"Khamespanah","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mohammed","family":"Gharib","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marjan","family":"Sirjani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ali","family":"Movaghar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,6,30]]},"reference":[{"key":"579_CR1","doi-asserted-by":"crossref","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), Proceedings 10th International Workshop on the Foundations of Coordination Languages and Software Architectures, FOCLASA 2011, Aachen, Germany, 10th September, 2011, volume\u00a058 of EPTCS, pp. 1\u201319 (2011)","DOI":"10.4204\/EPTCS.58.1"},{"key":"579_CR2","doi-asserted-by":"crossref","unstructured":"Agha, G., Hewitt, C.: Concurrent programming using actors: exploiting large-scale parallelism. In: Maheshwari, S.N. (ed) Foundations of Software Technology and Theoretical Computer Science, Fifth Conference, New Delhi, India, December 16-18, 1985, Proceedings, volume 206 of Lecture Notes in Computer Science, pp. 19\u201341. Springer (1985)","DOI":"10.1007\/3-540-16042-6_2"},{"key":"579_CR3","doi-asserted-by":"crossref","unstructured":"Aoxueluo, W., Weigang, C., Jiannong, R.M.: A generalized mutual exclusion problem and its algorithm. In: ICPP, pp. 300\u2013309. IEEE Computer Society (2013)","DOI":"10.1109\/ICPP.2013.39"},{"issue":"5","key":"579_CR4","doi-asserted-by":"publisher","first-page":"76:1","DOI":"10.1145\/3122848","volume":"50","author":"FS de Boer","year":"2017","unstructured":"de Boer, F.S., Serbanescu, V., H\u00e4hnle, R., Henrio, L., Rochas, J., Din, C.C., Johnsen, E.B., Sirjani, M., Khamespanah, E., Fernandez-Reyes, K., Yang, A.M.: A survey of active object languages. ACM Comput. Surv. 50(5), 76:1\u201376:39 (2017)","journal-title":"ACM Comput. Surv."},{"key":"579_CR5","doi-asserted-by":"crossref","unstructured":"Ferreira, B.B., Fernando A.F., Loureiro, Antonio A.F., Campos, S\u00e9rgio V.A.: A probabilistic model checking analysis of vehicular ad-hoc networks. In: IEEE 81st Vehicular Technology Conference, VTC Spring 2015, Glasgow, United Kingdom, 11\u201314 May, 2015, pp. 1\u20137. IEEE (2015)","DOI":"10.1109\/VTCSpring.2015.7145641"},{"key":"579_CR6","doi-asserted-by":"crossref","unstructured":"Gama, \u00d3., Nicolau, M.\u00a0J., Costa, A., Santos, A., Macedo, J., Dias, B.: Evaluation of message dissemination methods in vanets using a cooperative traffic efficiency application. In: IWCMC, pp. 478\u2013483. IEEE (2017)","DOI":"10.1109\/IWCMC.2017.7986332"},{"key":"579_CR7","unstructured":"Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design patterns: elements of reusable object-oriented software. Addison-Wesley Longman Publishing Co., Inc, Boston, MA, USA (1995)"},{"key":"579_CR8","doi-asserted-by":"crossref","unstructured":"Gholibeigi, M., Heijenk, G.: Analysis of multi-hop broadcast in vehicular ad hoc networks: a reliability perspective. In: Wireless Days, pp. 1\u20138. IEEE (2016)","DOI":"10.1109\/WD.2016.7461489"},{"issue":"3","key":"579_CR9","doi-asserted-by":"publisher","first-page":"1162","DOI":"10.1109\/TITS.2013.2252901","volume":"14","author":"MR Hafner","year":"2013","unstructured":"Hafner, M.R., Cunningham, D., Caminiti, L., Vecchio, D.D.: Cooperative collision avoidance at intersections: algorithms and experiments. IEEE Trans. Intell. Transp. Syst. 14(3), 1162\u20131175 (2013)","journal-title":"IEEE Trans. Intell. Transp. Syst."},{"key":"579_CR10","doi-asserted-by":"publisher","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."},{"key":"579_CR11","doi-asserted-by":"crossref","unstructured":"Jahandideh, I., Ghassemi, F., Sirjani, M.: Hybrid rebeca: modeling and analyzing of cyber-physical systems. In: Chamberlain, R.\u00a0D., Taha, W., T\u00f6rngren, M. (eds), Cyber Physical Systems. Model-Based Design - 8th International Workshop, CyPhy 2018, and 14th International Workshop, WESE 2018, Turin, Italy, October 4-5, 2018, Revised Selected Papers, volume 11615 of Lecture Notes in Computer Science, pp. 3\u201327. Springer, (2018)","DOI":"10.1007\/978-3-030-23703-5_1"},{"key":"579_CR12","doi-asserted-by":"crossref","unstructured":"Khamespanah, E.: Modeling, Verification, and Analysis of Timed Actor-Based Models. PhD thesis, Computer Science, Menntavegi 1, 101 Reykjavk, 6 (2018)","DOI":"10.1016\/j.scico.2017.11.004"},{"key":"579_CR13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.scico.2017.11.004","volume":"153","author":"E Khamespanah","year":"2018","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. 153, 1\u201329 (2018)","journal-title":"Sci. Comput. Program."},{"key":"579_CR14","doi-asserted-by":"crossref","unstructured":"Khamespanah, E., Sirjani, M., Viswanathan, M., Khosravi, R.: Floating time transition system: more efficient analysis of timed actors. In: Formal Aspects of Component Software - 12th International Conference, FACS 2015, Niter\u00f3i, Brazil, October 14-16, 2015, Revised Selected Papers, pp. 237\u2013255 (2015)","DOI":"10.1007\/978-3-319-28934-2_13"},{"issue":"1","key":"579_CR15","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1080\/15472450.2014.889932","volume":"20","author":"S Lin","year":"2016","unstructured":"Lin, S., Maxemchuk, N.F.: The fail-safe operation of collaborative driving systems. J. Intell. Transp. Syst. 20(1), 88\u2013101 (2016)","journal-title":"J. Intell. Transp. Syst."},{"issue":"2","key":"579_CR16","doi-asserted-by":"publisher","first-page":"556","DOI":"10.1109\/TITS.2018.2828413","volume":"20","author":"T Saeed","year":"2019","unstructured":"Saeed, T., Mylonas, Y., Pitsillides, A., Papadopoulou, V., Lestas, M.: Modeling probabilistic flooding in vanets for optimal rebroadcast probabilities. IEEE Trans. Intell. Transp. Syst. 20(2), 556\u2013570 (2019)","journal-title":"IEEE Trans. Intell. Transp. Syst."},{"key":"579_CR17","doi-asserted-by":"crossref","unstructured":"Sanguesa, J.\u00a0A., Fogue, M., Garrido, P., Martinez, F.\u00a0J., Cano, J.-C., Calafate, C.M.T., Manzoni, P.: On the selection of optimal broadcast schemes in vanets. In MSWiM, pp. 411\u2013418. ACM (2013)","DOI":"10.1145\/2507924.2507935"},{"key":"579_CR18","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1016\/j.comcom.2015.01.017","volume":"60","author":"JA Sanguesa","year":"2015","unstructured":"Sanguesa, J.A., Fogue, M., Garrido, P., Martinez, F.J., Cano, J.-C., Calafate, C.M.T., Manzoni, P.: RTAD: a real-time adaptive dissemination system for vanets. Comput. Commun. 60, 53\u201370 (2015)","journal-title":"Comput. Commun."},{"key":"579_CR19","first-page":"8714142:1","volume":"2016","author":"JA Sanguesa","year":"2016","unstructured":"Sanguesa, J.A., Fogue, M., Garrido, P., Martinez, F.J., Cano, J.-C., Calafate, C.T.: A survey and comparative study of broadcast warning message dissemination schemes for vanets. Mob. Inf. Syst. 2016, 8714142:1\u20138714142:18 (2016)","journal-title":"Mob. Inf. Syst."},{"key":"579_CR20","doi-asserted-by":"crossref","unstructured":"Sirjani, M., Jaghoori, M.M.: Ten years of analyzing actors: rebeca experience. In: Formal Modeling: Actors, Open Systems, Biological Systems, volume 7000 of Lecture Notes in Computer Science, pp. 20\u201356. Springer (2011)","DOI":"10.1007\/978-3-642-24933-4_3"},{"issue":"4","key":"579_CR21","first-page":"385","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. Inf. 63(4), 385\u2013410 (2004)","journal-title":"Fundam. Inf."},{"key":"579_CR22","doi-asserted-by":"crossref","unstructured":"Suriyapaibonwattana, K., Pomavalai, C.: An Effective Safety Alert Broadcast Algorithm for VANET. In: 2008 International Symposium on Communications and Information Technologies, pp. 247\u2013250. IEEE (oct 2008)","DOI":"10.1109\/ISCIT.2008.4700192"},{"issue":"2\u20133","key":"579_CR23","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1023\/A:1013763825347","volume":"8","author":"Y-C Tseng","year":"2002","unstructured":"Tseng, Y.-C., Ni, S.-Y., Chen, Y.-S., Sheu, J.-P.: The broadcast storm problem in a mobile ad hoc network. Wirel. Netw. 8(2\u20133), 153\u2013167 (2002)","journal-title":"Wirel. Netw."},{"key":"579_CR24","doi-asserted-by":"crossref","unstructured":"Yousefi, B., Ghassemi, F., Khosravi, R.: Modeling and efficient verification of broadcasting actors. In: Fundamentals of Software Engineering\u20146th International Conference, FSEN 2015 Tehran, Iran, April 22\u201324, 2015, Revised Selected Papers, pp. 69\u201383 (2015)","DOI":"10.1007\/978-3-319-24644-4_5"},{"issue":"6","key":"579_CR25","doi-asserted-by":"publisher","first-page":"1051","DOI":"10.1007\/s00165-017-0429-z","volume":"29","author":"B Yousefi","year":"2017","unstructured":"Yousefi, B., Ghassemi, F., Khosravi, R.: Modeling and efficient verification of wireless ad hoc networks. Form. Asp. Comput. 29(6), 1051\u20131086 (2017)","journal-title":"Form. Asp. Comput."},{"issue":"6","key":"579_CR26","doi-asserted-by":"publisher","first-page":"1051","DOI":"10.1007\/s00165-017-0429-z","volume":"29","author":"B Yousefi","year":"2017","unstructured":"Yousefi, B., Ghassemi, F., Khosravi, R.: Modeling and efficient verification of wireless ad hoc networks. Form. Asp. Comput. 29(6), 1051\u20131086 (2017)","journal-title":"Form. Asp. Comput."},{"key":"579_CR27","doi-asserted-by":"crossref","unstructured":"Yousefi, F., Khamespanah, E., Gharib, M., Sirjani, M., Movaghar, A.: Verivanca: an actor-based framework for formal verification of warning message dissemination schemes in vanets. In: Biondi, Fabrizio, Given-Wilson, Thomas, Legay, Axel (eds) Model Checking Software\u201426th International Symposium, SPIN 2019, Beijing, China, July 15-16, 2019, Proceedings, volume 11636 of Lecture Notes in Computer Science, pp. 244\u2013259. Springer (2019)","DOI":"10.1007\/978-3-030-30923-7_14"},{"issue":"4","key":"579_CR28","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/s11235-010-9400-5","volume":"50","author":"S Zeadally","year":"2012","unstructured":"Zeadally, S., Hunt, R., Chen, Y.-S., Irwin, A., Hassan, A.: Vehicular ad hoc networks (VANETS): status, results, and challenges. Telecommun. Syst. 50(4), 217\u2013241 (2012)","journal-title":"Telecommun. Syst."}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-020-00579-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-020-00579-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-020-00579-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,6,29]],"date-time":"2021-06-29T23:52:51Z","timestamp":1625010771000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-020-00579-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,6,30]]},"references-count":28,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2020,10]]}},"alternative-id":["579"],"URL":"https:\/\/doi.org\/10.1007\/s10009-020-00579-8","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,6,30]]},"assertion":[{"value":"30 June 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}