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://doi.org/10.1007/978-3-030-81915-6_13
Using Afra in Different Domains by Tool Orchestration | SpringerLink
Skip to main content
Springer Nature Link
Log in

Using Afra in Different Domains by Tool Orchestration

  • Chapter
  • First Online:
Composing Model-Based Analysis Tools

Abstract

The formal modelling and verification of distributed systems represents a complex process in which multiple tools are involved. Rebeca is a language which is developed to make modelling and verification of distributed systems with asynchronous message passing easier. This chapter shows how different tool orchestration methods are used for developing different verification engines for Rebeca models. As the first step, the way of enabling performance evaluation for Rebeca models is shown. To this end, state spaces which are generated for Rebeca models are transformed to the input of a third party tool and the result of the verification is given to the modeller. The second one is developing a search-based optimisation for wireless sensors and actuators applications. Running the model checker in a loop with different input parameters helps in finding the optimum values for parameters with respect to a given optimisation goal. The third one is for safety verification and performance evaluation of collaborative autonomous machines of Volvo car. The verification is done through developing and evaluating models by the model checking tool and Volvo car simulator (VCE Simulator).

This case-study chapter illustrates concepts introduced in Chap. 5 and addresses Challenge 2 in Chap. 3 of this book.

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

Access this chapter

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

eBook
USD 15.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.00
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 159.00
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Gul A. Agha. ACTORS - A Model of Concurrent Computation in Distributed Systems. MIT Press.

    Google Scholar 

  2. Gul Agha and Carl Hewitt. “Concurrent programming using actors”. In: (1987), pp. 37–53.

    Google Scholar 

  3. Akka. Typesafe, Inc. Akka. 2009.

    Google Scholar 

  4. Giorgio Forcina, Ali Sedaghatbaf, Stephan Baumgart, Ali Jafari, Ehsan Khamespanah, Pavle Mrvaljevic, and Marjan Sirjani. “Safe Design of Flow Management Systems Using Rebeca”. In: Journal of Information Processing 28 (2020), pp. 588– 598. https://doi.org/10.2197/ipsjjip.28.588.

  5. Dennis Guck, Tingting Han, Joost-Pieter Katoen, and Martin R. Neuhäußer. “Quantitative timed analysis of interactive Markov chains”. In: 4th international conference on NASA Formal Methods. 2012, pp. 8–23.

    Google Scholar 

  6. Robert Heinrich, Francisco Durán, Carolyn L. Talcott, and Steffen Zschaler (eds.) Composing Model-Based Analysis Tools. Springer, 2021. https://doi.org/10.1007/978-3-030-81915-6.

  7. C. Hewitt. 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, 1972.

    Google Scholar 

  8. Ali Jafari, Ehsan Khamespanah, Marjan Sirjani, and Holger Hermanns. “Performance Analysis of Distributed and Asynchronous Systems using Probabilistic Timed Actors”. In: (2014). http://journal.ub.tu-berlin.de/eceasst/article/view/984.

  9. Ali Jafari, Ehsan Khamespanah, Marjan Sirjani, Holger Hermanns, and Matteo Cimini. “PTRebeca: Modeling and analysis of distributed and asynchronous systems”. In: Science of Computer Programming 128 (2016), pp. 22–50.

    Google Scholar 

  10. Ehsan Khamespanah, Marjan Sirjani, Mahesh Viswanathan, and Ramtin Khosravi. “Floating Time Transition System: More Efficient Analysis of Timed Actors”. In: 12th International Conference Formal Aspects of Component Software. 2015, pp. 237–255. https://doi.org/10.1007/978-3-319-28934-2_13.

  11. Ehsan Khamespanah, Marjan Sirjani, Kirill Mechitov, and Gul Agha. “Modeling and analyzing real-time wireless sensor and actuator networks using actors and model checking”. In: International Journal on Software Tools for Technology Transfer 20.5 (2018), pp. 547–561.

    Google Scholar 

  12. Ehsan Khamespanah, Ramtin Khosravi, and Marjan Sirjani. “An efficient TCTL model checking algorithm and a reduction technique for verification of timed actor models”. In: Science of Computer Programming 153 (2018), pp. 1–29.

    Google Scholar 

  13. Pavle Mrvaljevic. Tool Orchestration for Modeling, Verification, and Analysis of Collaborating Autonomous Machines. Master Thesis. Mälardalen University, 2020.

    Google Scholar 

  14. Peter Csaba Ölveczky and José Meseguer. “Semantics and pragmatics of Real-Time Maude”. In: Higher-Order and Symbolic Computation 20.1-2 (2007), pp. 161–196.

    Google Scholar 

  15. Morgan Quigley, Ken Conley, Brian Gerkey, Josh Faust, Tully Foote, Jeremy Leibs, Rob Wheeler, and Andrew Y Ng. “Workshop on Open Source Software in Robotics”. In: vol. 3. 3.2. 2009, p. 5.

    Google Scholar 

  16. Arni Hermann Reynisson, Marjan Sirjani, Luca Aceto, Matteo Cimini, Ali Jafari, Anna Ingólfsdóttir, and Steinar Hugi Sigurdarson. “Modelling and Simulation of Asynchronous Real-Time Systems Using Timed Rebeca”. In: Science of Computer Programming 89 (2014), pp. 41–68.

    Google Scholar 

  17. Marjan Sirjani, Ali Movaghar, Amin Shali, and Frank S. de Boer. “Modeling and Verification of Reactive Systems using Rebeca”. In: Fundamenta Informaticae 63.4 (2004), pp. 385–410.

    Google Scholar 

  18. Marjan Sirjani, Giorgio Forcina, Ali Jafari, Stephan Baumgart, Ehsan Khamespanah, and Ali Sedaghatbaf. “An Actor-Based Design Platform for System of Systems”. In: 43rd IEEE Annual Computer Software and Applications Conference. 2019, pp. 579–587. https://doi.org/10.1109/COMPSAC.2019.00089.

  19. Marjan Sirjani and Ehsan Khamespanah. “On Time Actors”. In: Theory and Practice of Formal Methods - Essays Dedicated to Frank de Boer on the Occasion of His 60th Birthday. 2016, pp. 373–392. https://doi.org/10.1007/978-3-319-30734-3_25.

  20. Mahsa Varshosaz and Ramtin Khosravi. “Modeling and Verification of Probabilistic Actor Systems Using pRebeca”. In: 14th International Conference on Formal Engineering Methods. 2012, pp. 135–150. https://doi.org/10.1007/978-3-642-34281-3_12.

  21. Farnaz Yousefi, Ehsan Khamespanah, Mohammed Gharib, Marjan Sirjani, and Ali Movaghar. “VeriVANca framework: verification of VANETs by property-based message passing of actors in Rebeca with inheritance”. In: International Journal on Software Tools for Technology Transfer 22.5 (2020), pp. 617–633. https://doi.org/10.1007/s10009-020-00579-8.

Download references

Author information

Authors and Affiliations

  1. University of Tehran, Tehran, Iran

    Ehsan Khamespanah

  2. Mälardalen University, Västerås, Sweden

    Pavle Mrvaljevic, Anas Fattouh & Marjan Sirjani

Authors
  1. Ehsan Khamespanah
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Pavle Mrvaljevic
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Anas Fattouh
    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

Corresponding author

Correspondence to Ehsan Khamespanah .

Editor information

Editors and Affiliations

  1. Karlsruhe Institute of Technology, Karlsruhe, Germany

    Robert Heinrich

  2. University of Málaga, Málaga, Spain

    Francisco Durán

  3. SRI International, Menlo Park, CA, USA

    Carolyn Talcott

  4. King's College London, London, UK

    Steffen Zschaler

Rights and permissions

Reprints and permissions

Copyright information

© 2021 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Khamespanah, E., Mrvaljevic, P., Fattouh, A., Sirjani, M. (2021). Using Afra in Different Domains by Tool Orchestration. In: Heinrich, R., Durán, F., Talcott, C., Zschaler, S. (eds) Composing Model-Based Analysis Tools. Springer, Cham. https://doi.org/10.1007/978-3-030-81915-6_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-81915-6_13

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-81914-9

  • Online ISBN: 978-3-030-81915-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation