iBet uBet web content aggregator. Adding the entire web to your favor.
iBet uBet web content aggregator. Adding the entire web to your favor.



Link to original content: https://unpaywall.org/10.1007/S10009-020-00579-8
VeriVANca framework: verification of VANETs by property-based message passing of actors in Rebeca with inheritance | International Journal on Software Tools for Technology Transfer Skip to main content
Springer Nature Link
Log in

VeriVANca framework: verification of VANETs by property-based message passing of actors in Rebeca with inheritance

  • STTT
  • Special Issue: SPIN 2019
  • Published:
International Journal on Software Tools for Technology Transfer Aims and scope Submit manuscript

Abstract

Vehicular ad hoc networks have attracted the attention of many researchers during the last years due to the emergence of autonomous vehicles and safety concerns. Most of the frameworks which are proposed for the modeling and analysis VANET applications make use of simulation techniques. Due to the high level of concurrency in these applications, simulation results do not guarantee the correct behavior of the system and more accurate analysis techniques are required. In this paper, we have developed a framework to provide model checking facilities for the analysis of VANET applications. To this end, an actor-based modeling language, Rebeca, is used which is equipped with a variety of model checking engines. We have extended Rebeca with the inheritance mechanism to support model-specific message passing among vehicles, which is crucial for the modeling of VANET applications. To illustrate the applicability of this framework, we modeled and analyzed two warning message dissemination schemes. Reviewing the results of using the model checking technique supports the claim that concurrent behaviors of the system components in VANETs may cause uncertainty which may not be detected by simulation-based techniques. We also observed that considering the interleaving of concurrent executions of the system components affects the performance metrics of it.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8

Similar content being viewed by others

Explore related subjects

Discover the latest articles, news and stories from top researchers in related subjects.

References

  1. Aceto, L., Cimini, M., Ingólfsdóttir, 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 58 of EPTCS, pp. 1–19 (2011)

  2. 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–41. Springer (1985)

  3. Aoxueluo, W., Weigang, C., Jiannong, R.M.: A generalized mutual exclusion problem and its algorithm. In: ICPP, pp. 300–309. IEEE Computer Society (2013)

  4. de Boer, F.S., Serbanescu, V., Hähnle, 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–76:39 (2017)

    Article  Google Scholar 

  5. Ferreira, B.B., Fernando A.F., Loureiro, Antonio A.F., Campos, Sérgio 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–14 May, 2015, pp. 1–7. IEEE (2015)

  6. Gama, Ó., Nicolau, M. J., 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–483. IEEE (2017)

  7. 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)

  8. Gholibeigi, M., Heijenk, G.: Analysis of multi-hop broadcast in vehicular ad hoc networks: a reliability perspective. In: Wireless Days, pp. 1–8. IEEE (2016)

  9. 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–1175 (2013)

    Article  Google Scholar 

  10. Jafari, A., Khamespanah, E., Sirjani, M., Hermanns, H., Cimini, M.: Ptrebeca: modeling and analysis of distributed and asynchronous systems. Sci. Comput. Program. 128, 22–50 (2016)

    Article  Google Scholar 

  11. Jahandideh, I., Ghassemi, F., Sirjani, M.: Hybrid rebeca: modeling and analyzing of cyber-physical systems. In: Chamberlain, R. D., Taha, W., Törngren, 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–27. Springer, (2018)

  12. Khamespanah, E.: Modeling, Verification, and Analysis of Timed Actor-Based Models. PhD thesis, Computer Science, Menntavegi 1, 101 Reykjavk, 6 (2018)

  13. 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–29 (2018)

    Article  Google Scholar 

  14. 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ói, Brazil, October 14-16, 2015, Revised Selected Papers, pp. 237–255 (2015)

  15. Lin, S., Maxemchuk, N.F.: The fail-safe operation of collaborative driving systems. J. Intell. Transp. Syst. 20(1), 88–101 (2016)

    Article  Google Scholar 

  16. 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–570 (2019)

    Article  Google Scholar 

  17. Sanguesa, J. A., Fogue, M., Garrido, P., Martinez, F. J., Cano, J.-C., Calafate, C.M.T., Manzoni, P.: On the selection of optimal broadcast schemes in vanets. In MSWiM, pp. 411–418. ACM (2013)

  18. 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–70 (2015)

    Article  Google Scholar 

  19. 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–8714142:18 (2016)

    Google Scholar 

  20. 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–56. Springer (2011)

  21. Sirjani, M., Movaghar, A., Shali, A., De Boer, F.S.: Modeling and verification of reactive systems using rebeca. Fundam. Inf. 63(4), 385–410 (2004)

    MathSciNet  MATH  Google Scholar 

  22. Suriyapaibonwattana, K., Pomavalai, C.: An Effective Safety Alert Broadcast Algorithm for VANET. In: 2008 International Symposium on Communications and Information Technologies, pp. 247–250. IEEE (oct 2008)

  23. 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–3), 153–167 (2002)

    Article  Google Scholar 

  24. Yousefi, B., Ghassemi, F., Khosravi, R.: Modeling and efficient verification of broadcasting actors. In: Fundamentals of Software Engineering—6th International Conference, FSEN 2015 Tehran, Iran, April 22–24, 2015, Revised Selected Papers, pp. 69–83 (2015)

  25. Yousefi, B., Ghassemi, F., Khosravi, R.: Modeling and efficient verification of wireless ad hoc networks. Form. Asp. Comput. 29(6), 1051–1086 (2017)

    Article  MathSciNet  Google Scholar 

  26. Yousefi, B., Ghassemi, F., Khosravi, R.: Modeling and efficient verification of wireless ad hoc networks. Form. Asp. Comput. 29(6), 1051–1086 (2017)

    Article  MathSciNet  Google Scholar 

  27. 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—26th International Symposium, SPIN 2019, Beijing, China, July 15-16, 2019, Proceedings, volume 11636 of Lecture Notes in Computer Science, pp. 244–259. Springer (2019)

  28. 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–241 (2012)

    Article  Google Scholar 

Download references

Acknowledgements

The work on this paper has been supported in part by the project “Self-Adaptive Actors: SEADA” (163205-051) of the Icelandic Research Fund and by DPAC Project (Dependable Platforms for Autonomous Systems and Control) at Mälardalen University, Sweden.

Author information

Authors and Affiliations

  1. Department of Computer Engineering, Sharif University of Technology, Tehran, Iran

    Farnaz Yousefi & Ali Movaghar

  2. School of Electrical and Computer Engineering, University of Tehran, Tehran, Iran

    Ehsan Khamespanah

  3. School of Computer Science, Reykjavik University, Reykjavik, Iceland

    Ehsan Khamespanah & Marjan Sirjani

  4. School of Computer Science, Institute for Research in Fundamental Science (IPM), Tehran, Iran

    Mohammed Gharib

  5. School of IDT, Mälardalen University, Västersås, Sweden

    Marjan Sirjani

Authors
  1. Farnaz Yousefi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ehsan Khamespanah
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Mohammed Gharib
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Marjan Sirjani
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Ali Movaghar
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Ehsan Khamespanah.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Yousefi, F., Khamespanah, E., Gharib, M. et al. VeriVANca framework: verification of VANETs by property-based message passing of actors in Rebeca with inheritance. Int J Softw Tools Technol Transfer 22, 617–633 (2020). https://doi.org/10.1007/s10009-020-00579-8

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10009-020-00579-8

Keywords

Search

Navigation