Skip to main content
SpringerLink
Log in
Book cover

International Conference on Software Engineering and Formal Methods

SEFM 2016: Software Engineering and Formal Methods pp 3–8Cite as

Abstractions, Semantic Models and Analysis Tools for Concurrent Systems: Progress and Open Problems

(Extended Abstract)

  • Conference paper
  • First Online:

  • 914 Accesses

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9763))

Abstract

The growth of mobile and cloud computing, cyberphysical systems and the internet of things has arguably made scalable concurrency the central to computing. Actor languages and frameworks have been widely adopted to address scalability. Moreover, new tools that combine static and dyamic analysis are making software safer. This presentation describes the actor programming model and reasoning tools for scalable concurrency. As we scale up cyberphysical applications and build the internet of things, a key limitation of current languages and tools becomes apparent: the difficulty of representing quantitative and probabilistic properties and reasoning about them. The paper concludes by discussing some techniques to address reasoning about the behavior of complex scalable concurrent applications.

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

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight 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

Learn about institutional subscriptions

Notes

  1. 1.

    Although the term first appears in [24].

  2. 2.

    http://research.microsoft.com/en-us/projects/pex/.

References

  1. Building Halo 4, a video game, using the actor model. http://www.infoq.com/news/2015/03/halo4-actor-model

  2. Dart. http://www.dartlang.org

  3. Erlang-powered Whatsapp. https://www.erlang-solutions.com/about/news/erlang-powered-whatsapp-exceeds-200-million-monthly-users

  4. Erlang programming language

    Google Scholar 

  5. Facebook chat. https://www.facebook.com/note.php?note_id=14218138919

  6. How and why Twitter uses Scala. https://www.redfin.com/devblog/2010/05/how_and_why_twitter_uses_scala.html

  7. NHS to deploy Riak for new IT backbone. http://basho.com/posts/press/nhs-to-deploy-riak-for-new-it-backbone-with-quality-of-care-improvements-in-sight/

  8. Agha, G., Gunter, C., Greenwald, M., Khanna, S., Meseguer, J., Sen, K., Thati, P.: Formal modeling and analysis of DOS using probabilistic rewrite theories. In: Workshop on Foundations of Computer Security (FCS 2005), vol. 20, pp. 1–15 (2005)

    Google Scholar 

  9. Agha, G., Houck, C.R., Panwar, R.: Distributed execution of actor programs. In: Banerjee, U., Gelernter, D., Nicolau, A., Padua, D.A. (eds.) Languages and Compilers for Parallel Computing. LNCS, vol. 589, pp. 1–17. Springer, Heidelberg (1992)

    Chapter  Google Scholar 

  10. Agha, G., Mason, I.A., Smith, S.F., Talcott, C.L.: A foundation for actor computation. J. Funct. Program. 7(1), 1–72 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  11. Agha, G., Meseguer, J., Sen, K.: PMaude: rewrite-based specification language for probabilistic object systems. Electron. Notes Theoret. Comput. Sci. 153(2), 213–239 (2006)

    Article  Google Scholar 

  12. Agha, G.A.: ACTORS - A Model of Concurrent Computation in Distributed Systems. MIT Press Series in Artificial Intelligence. MIT Press, Cambridge (1990)

    Google Scholar 

  13. Bernstein, P.A., Bykov, S., Geller, A., Kliot, G., Thelin, J.: Orleans: distributed virtual actors for programmability and scalability. Technical report MSR-TR-2014-41, Microsoft Research (2014)

    Google Scholar 

  14. Dinges, P., Agha, G.: Solving complex path conditions through heuristic search on induced polytopes. In: Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2014, pp. 425–436. ACM (2014)

    Google Scholar 

  15. Godefroid, P., Klarlund, N., Sen, K.: Dart: directed automated random testing. In: Sarkar, V., Hall, M.W. (eds.) PLDI, pp. 213–223. ACM (2005)

    Google Scholar 

  16. Jamali, N., Thati, P., Agha, G.A.: An actor-based architecture for customizing and controlling agent ensembles. IEEE Intell. Syst. 2, 38–44 (1999)

    Article  Google Scholar 

  17. Kwon, Y., Agha, G.: Verifying the evolution of probability distributions governed by a DTMC. IEEE Trans. Softw. Eng. 37(1), 126–141 (2011)

    Article  Google Scholar 

  18. Kwon, Y., Agha, G.: Performance evaluation of sensor networks by statistical modeling and Euclidean model checking. ACM Trans. Sensor Netw. 9(4), 39:1–39:38 (2013)

    Article  Google Scholar 

  19. Lauterburg, S., Karmani, R.K., Marinov, D., Agha, G.: Basset: a tool for systematic testing of actor programs. In: Roman, G.-C., Sullivan, K.J. (eds.) 2010 Proceedings of the 18th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 7–11 November 2010, Santa Fe, NM, USA, pp. 363–364. ACM (2010)

    Google Scholar 

  20. Ren, S., Agha, G.: RTsynchronizer: language support for real-time specifications in distributed systems. In: Gerber, R., Marlowe, T.J. (eds.) Proceedings of the ACM SIGPLAN 1995 Workshop on Languages, Compilers, & Tools for Real-Time Systems (LCT-RTS 1995), 21–22 June 1995, La Jolla, California, pp. 50–59. ACM (1995)

    Google Scholar 

  21. Sen, K., Agha, G.: CUTE and jCUTE: concolic unit testing and explicit path model-checking tools. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 419–423. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  22. Sen, K., Agha, G.: Automated systematic testing of open distributed programs. In: Baresi, L., Heckel, R. (eds.) FASE 2006. LNCS, vol. 3922, pp. 339–356. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  23. Sen, K., Agha, G.: A race-detection and flipping algorithm for automated testing of multi-threaded programs. In: Bin, E., Ziv, A., Ur, S. (eds.) HVC 2006. LNCS, vol. 4383, pp. 166–182. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  24. Sen, K., Marinov, D., Agha, G.: Cute: a concolic unit testing engine for C. In: Wermelinger, M., Gall, H. (eds.) Proceedings of the 10th European Software Engineering Conference held jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 5–9 September 2005, Lisbon, Portugal, pp. 263–272. ACM (2005)

    Google Scholar 

  25. Sen, K., Viswanathan, M., Agha, G.: Statistical model checking of black-box probabilistic systems. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 202–215. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  26. Sen, K., Viswanathan, M., Agha, G.: Vesta: a statistical model-checker and analyzer for probabilistic systems. In: Second International Conference on the Quantitative Evaluaiton of Systems (QEST 2005), 19–22 September 2005, Torino, Italy, pp. 251–252. IEEE Computer Society (2005)

    Google Scholar 

Download references

Acknowledgements

The work on this paper has been supported in part by Air Force Research Laboratory and the Air Force Office of Scientific Research under agreement number FA8750-11-2-0084, and by National Science Foundation under grant number CCF-1438982.

Author information

Authors and Affiliations

  1. University of Illinois at Urbana-Champaign, Champaign, USA

    Gul Agha

Authors
  1. Gul Agha
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Gul Agha .

Editor information

Editors and Affiliations

  1. IMT - School for Advanced Studies, Lucca, Italy

    Rocco De Nicola

  2. Institute of Computer Languages, TU Wien, Wien, Austria

    Eva Kühn

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Agha, G. (2016). Abstractions, Semantic Models and Analysis Tools for Concurrent Systems: Progress and Open Problems. In: De Nicola, R., Kühn, E. (eds) Software Engineering and Formal Methods. SEFM 2016. Lecture Notes in Computer Science(), vol 9763. Springer, Cham. https://doi.org/10.1007/978-3-319-41591-8_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-41591-8_1

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-41590-1

  • Online ISBN: 978-3-319-41591-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation