Abstraction and Verification of Properties of a Real-Time Java | SpringerLink
Skip to main content

Abstraction and Verification of Properties of a Real-Time Java

  • Conference paper
ICT in Education, Research, and Industrial Applications (ICTERI 2012)

Abstract

We present a tool for analysing resource sharing conflicts in multithreaded Java programs. Java programs are translated to timed automata models verified afterwards by the Uppaal model checker. Analysed programs are annotated with timing information indicating the execution duration of a particular statement. Based on the timing information, the analysis of execution paths is performed, which gives an answer whether resource sharing conflicts are possible in a multithreaded Java program. If the analysis succeeds, resource locks may be eliminated from the Java program.

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

Access this chapter

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 5719
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 7149
Price includes VAT (Japan)
  • 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

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. Baklanova, N., Strecker, M., Féraud, L.: Resource sharing conflicts checking in multithreaded Java programs. In: Journées FAC 2012 (2012)

    Google Scholar 

  2. Fersman, E., Mokrushin, L., Pettersson, P., Yi, W.: Schedulability analysis of fixed-priority systems using timed automata. Theor. Comput. Sci. 354, 301–317 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  3. Bøgholm, T., Kragh-Hansen, H., Olsen, P.: Model based schedulability analysis of real-time systems. Master’s thesis, Aalborg University (2008)

    Google Scholar 

  4. Bøgholm, T., Kragh-Hansen, H., Olsen, P., Thomsen, B., Larsen, K.G.: Model-based schedulability analysis of safety critical hard real-time Java programs. In: Bollella, G., Locke, C.D. (eds.) JTRES. ACM International Conference Proceeding Series, vol. 343, pp. 106–114. ACM (2008)

    Google Scholar 

  5. Hakimipour, N., Strooper, P., Wellings, A.: A model-based development approach for the verification of real-time java code. Concurrency and Computation: Practice and Experience 23(13), 1583–1606 (2011)

    Article  Google Scholar 

  6. Herber, P., Pockrandt, M., Glesner, S.: Transforming systemc transaction level models into uppaal timed automata. In: 2011 9th IEEE/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE), pp. 161–170 (2011)

    Google Scholar 

  7. Cordovilla, M., Boniol, F., Noulard, E., Pagetti, C.: Multiprocessor schedulability analyser. In: Chu, W.C., Wong, W.E., Palakal, M.J., Hung, C.C. (eds.) SAC, pp. 735–741. ACM (2011)

    Google Scholar 

  8. Ravn, A.P., Schoeberl, M.: Cyclic executive for safety-critical java on chip-multiprocessors. In: Kalibera, T., Vitek, J. (eds.) JTRES. ACM International Conference Proceeding Series, pp. 63–69. ACM (2010)

    Google Scholar 

  9. Vechev, M., Yahav, E., Raman, R., Sarkar, V.: Automatic Verification of Determinism for Structured Parallel Programs. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 455–471. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  10. Tofan, B., Schellhorn, G., Bäumler, S., Reif, W.: Embedding rely-guarantee reasoning in temporal logic. Technical Report 2010-07, Informatik (2010)

    Google Scholar 

  11. The Real-Time for Java Expert Group: The Real-Time Specification for Java (2006)

    Google Scholar 

  12. The Open Group JSR: JSR-302 Safety Critical Java Technology Specification (2010), http://jcp.org/en/jsr/detail?id=308

  13. Henties, T., Hunt, J.J., Locke, D., Nilsen, K., Schoeberl, M., Vitek, J.: Java for safety-critical applications. In: 2nd International Workshop on the Certification of Safety-Critical Software Controlled Systems, SafeCert 2009 (March 2009)

    Google Scholar 

  14. Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126, 183–235 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  15. Bengtsson, J.E., Yi, W.: Timed Automata: Semantics, Algorithms and Tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) ACPN 2003. LNCS, vol. 3098, pp. 87–124. Springer, Heidelberg (2004), http://dx.doi.org/10.1007/978-3-540-27755-2_3

    Google Scholar 

  16. Alur, R., Courcoubetis, C., Dill, D.: Model-checking for real-time systems. In: Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, LICS 1990, pp. 414–425 (June 1990)

    Google Scholar 

  17. Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press (2008)

    Google Scholar 

  18. Henzinger, T.A., Horowitz, B., Kirsch, C.M.: Giotto: a time-triggered language for embedded programming. Proceedings of the IEEE 91(1), 84–99 (2003)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Baklanova, N., Strecker, M. (2013). Abstraction and Verification of Properties of a Real-Time Java. In: Ermolayev, V., Mayr, H.C., Nikitchenko, M., Spivakovsky, A., Zholtkevych, G. (eds) ICT in Education, Research, and Industrial Applications. ICTERI 2012. Communications in Computer and Information Science, vol 347. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-35737-4_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-35737-4_1

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-35736-7

  • Online ISBN: 978-3-642-35737-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics