Skip to main content
SpringerLink
Log in
Book cover

Models, Algorithms, Logics and Tools pp 269–288Cite as

Firm Deadline Checking of Safety-Critical Java Applications with Statistical Model Checking

  • Chapter
  • First Online:

  • 1174 Accesses

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

Abstract

In cyber-physical applications many programs have hard real-time constraints that have to be stringently validated. In some applications, there are programs that have hard deadlines, which must not be violated. Other programs have soft deadlines where the value of the response decreases when the deadline is passed although it is still a valid response. In between, there are programs with firm deadlines. Here the response may be occasionally delayed; but this should not happen too often or with too large an overshoot. This paper presents an extension to an existing approach and tool for checking hard deadline constraints to the case of firm deadlines for application programs written in Safety-Critical Java (SCJ). The existing approach uses models and model checking with the Uppaal toolset; the extension uses the statistical model checking features of Uppaal-smc to provide a hold on firm deadlines and performance in the case of soft deadlines. The extended approach is illustrated with examples from 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.

    The tool can be obtained at http://people.cs.aau.dk/~boegholm/tetasarts/.

  2. 2.

    In case of identical deadlines, one can safely arbitrarily assign different priorities, as long as these do not violate the priority of other tasks.

References

  1. Amnell, T., Fersman, E., Mokrushin, L., Pettersson, P., Yi, W.: TIMES: a tool for schedulability analysis and code generation of real-time systems. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol. 2791, pp. 60–72. Springer, Heidelberg (2004). doi:10.1007/978-3-540-40903-8_6

    Chapter  Google Scholar 

  2. Audsley, N., Burns, A., Richardson, M., Tindell, K., Wellings, A.J.: Applying new scheduling theory to static priority pre-emptive scheduling. Softw. Eng. J. 8(5), 284–292 (1993)

    Article  Google Scholar 

  3. Bengtsson, J., Larsen, K., Larsson, F., Pettersson, P., Yi, W.: UPPAAL — a tool suite for automatic verification of real-time systems. In: Alur, R., Henzinger, T.A., Sontag, E.D. (eds.) HS 1995. LNCS, vol. 1066, pp. 232–243. Springer, Heidelberg (1996). doi:10.1007/BFb0020949

    Chapter  Google Scholar 

  4. Bernat, G., Burns, A., Llamosí, A.: Weakly hard real-time systems. IEEE Trans. Comput. 50(4), 308–321 (2001)

    Article  MathSciNet  Google Scholar 

  5. Bøgholm, T., Hansen, R.R., Ravn, A.P., Thomsen, B., Søndergaard, H.: A predictable Java profile - rationale and implementations. In: Proceedings of the 7th International Workshop on Java Technologies for Real-Time and Embedded Systems, JTRES 2009, pp. 150–159 (2009)

    Google Scholar 

  6. 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: Proceedings of the 6th International Workshop on Java Technologies for Real-time and Embedded Systems, JTRES 2008, pp. 106–114 (2008)

    Google Scholar 

  7. Bollella, G.: The Real-time Specification for Java. Addison-Wesley Java Series. Addison-Wesley, Boston (2000)

    Google Scholar 

  8. Burns, A., Wellings, A.: Real-Time Systems and Programming Languages: ADA 95, Real-Time Java, and Real-Time POSIX, 4th edn. Addison-Wesley Educational Publishers Inc., Boston (2009)

    Google Scholar 

  9. Bøgholm, T., Hansen, R.R., Ravn, A.P., Thomsen, B., Søndergaard, H.: Schedulability analysis for Java finalizers. In: Proceedings of the 8th International Workshop on Java Technologies for Real-Time and Embedded Systems, JTRES 2010, pp. 1–7. ACM, New York (2010)

    Google Scholar 

  10. Dalsgaard, A.E., Olesen, M.C., Toft, M., Hansen, R.R., Larsen, K.G.: METAMOC: modular execution time analysis using model checking. In: 10th International Workshop on Worst-Case Execution Time Analysis (2010)

    Google Scholar 

  11. David, A., Larsen, K.G., Legay, A., Mikučionis, M., Poulsen, D.B., Vliet, J., Wang, Z.: Statistical model checking for networks of priced timed automata. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 80–96. Springer, Heidelberg (2011). doi:10.1007/978-3-642-24310-3_7

    Chapter  Google Scholar 

  12. David, A., Larsen, K.G., Legay, A., Mikučionis, M., Wang, Z.: Time for statistical model checking of real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 349–355. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22110-1_27

    Chapter  Google Scholar 

  13. David, A., Larsen, K.G., Legay, A., Mikučionis, M.: Schedulability of herschel-planck revisited using statistical model checking. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012. LNCS, vol. 7610, pp. 293–307. Springer, Heidelberg (2012). doi:10.1007/978-3-642-34032-1_28

    Chapter  Google Scholar 

  14. Davis, R.I., Burns, A.: A survey of hard real-time scheduling for multiprocessor systems. ACM Comput. Surv. 43(4), 35:1–35:44 (2011)

    Article  MATH  Google Scholar 

  15. Ferdinand, C.: Worst case execution time prediction by static program analysis. In: Proceedings of the 18th International Parallel and Distributed Processing Symposium, p. 125. IEEE (2004)

    Google Scholar 

  16. Frost, C., Jensen, C.S., Luckow, K.S., Thomsen, B.: WCET analysis of Java bytecode featuring common execution environments. In: 9th International Workshop on Java Technologies for Real-Time and Embedded Systems (2011)

    Google Scholar 

  17. Hansen, J.P., Hissam, S.A., Moreno, G.A.: Statistical-based WCET estimation and validation. In: 9th International Workshop on Worst-Case Execution Time Analysis, WCET 2009, Dublin, Ireland, 1–3 July 2009 (2009)

    Google Scholar 

  18. Hu, E.Y.-S., Wellings, A., Bernat, G.: XRTJ: an extensible distributed high-integrity real-time Java environment. In: Chen, J., Hong, S. (eds.) RTCSA 2003. LNCS, vol. 2968, pp. 208–228. Springer, Heidelberg (2004). doi:10.1007/978-3-540-24686-2_13

    Chapter  Google Scholar 

  19. Tri-Pacific Software Inc.: RAPID RMA (2013). http://www.tripac.com/rapid-rma

  20. Katoen, J.-P., Zapreev, I.S., Hahn, E.M., Hermanns, H., Jansen, D.N.: The ins and outs of the probabilistic model checker MRMC. Perform. Eval. 68(2), 90–104 (2011)

    Article  Google Scholar 

  21. Kyle, D., Hansen, J., Chaki, S.: Statistical model checking of distributed adaptive real-time software. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 269–274. Springer, Cham (2015). doi:10.1007/978-3-319-23820-3_17

    Chapter  Google Scholar 

  22. Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. Int. J. Softw. Tools Technol. Transf. (1997)

    Google Scholar 

  23. Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Roşu, G., Sokolsky, O., Tillmann, N. (eds.) RV 2010. LNCS, vol. 6418, pp. 122–135. Springer, Heidelberg (2010). doi:10.1007/978-3-642-16612-9_11

    Chapter  Google Scholar 

  24. Li, Y.-T.S., Malik, S.: Performance analysis of embedded software using implicit path enumeration. In: Proceedings of the 32nd Annual ACM/IEEE Design Automation Conference, DAC 1995, pp. 456–461. ACM, New York (1995)

    Google Scholar 

  25. Liu, D., Hu, X.S., Lemmon, M.D., Ling, Q.: Firm real-time system scheduling based on a novel QoS constraint. IEEE Trans. Computers 55(3), 320–333 (2006)

    Article  Google Scholar 

  26. Locke, D., Andersen, B.S., Brosgol, B., Fulton, M., Henties, T., Hunt, J.J., Nielsen, J.O., Nilsen, K., Schoeberl, M., Tokar, J., Vitek, J., Wellings, A.: Safety-Critical Java Technology Specification, Public draft (2013)

    Google Scholar 

  27. Luckow, K.S., Thomsen, B., Korsholm, S.E.: HVM-TP: a time predictable and portable Java virtual machine for hard real-time embedded systems. In: 12th International Workshop on Java Technologies for Real-Time and Embedded Systems (2014, to appear)

    Google Scholar 

  28. Luckow, K.S., Bøgholm, T., Thomsen, B., Larsen, K.G.: TetaSARTS: a tool for modular timing analysis of safety critical Java systems. In: Proceedings of the 11th International Workshop on Java Technologies for Real-Time and Embedded Systems, JTRES 2013, pp. 11–20 (2013)

    Google Scholar 

  29. Luckow, K.S., Thomsen, B., Korsholm, S.E.: HVMTP: a time predictable and portable java virtual machine for hard real-time embedded systems. Concurr. Comput.: Pract. Exp. (2016). cpe.3828

    Google Scholar 

  30. Schoeberl, M.: JOP: A Java Optimized Processor for Embedded Real-Time Systems. VDM Verlag Dr. Müller, Saarbrücken (2008). ISBN 978-3-8364-8086-4

    Google Scholar 

  31. Mikučionis, M., Larsen, K.G., Rasmussen, J.I., Nielsen, B., Skou, A., Palm, S.U., Pedersen, J.S., Hougaard, P.: Schedulability analysis using Uppaal: Herschel-Planck case study. In: Margaria, T., Steffen, B. (eds.) ISoLA 2010. LNCS, vol. 6416, pp. 175–190. Springer, Heidelberg (2010). doi:10.1007/978-3-642-16561-0_21

    Chapter  Google Scholar 

  32. Plsek, A., Zhao, L., Sahin, V.H., Tang, D., Kalibera, T., Vitek, J.: Developing safety critical Java applications with oSCJ/L0. In: Proceedings of the 8th International Workshop on Java Technologies for Real-Time and Embedded Systems, JTRES 2010, pp. 95–101. ACM, New York (2010)

    Google Scholar 

  33. Schoeberl, M., Puffitsch, W., Pedersen, R.U., Huber, B.: Worst-case execution time analysis for a Java processor. Softw.: Pract. Exp. 40(6), 507–542 (2010)

    Google Scholar 

  34. 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). doi:10.1007/978-3-540-27813-9_16

    Chapter  Google Scholar 

  35. Wilhelm, R., Engblom, J., Ermedahl, A., Holsti, N., Thesing, S., Whalley, D., Bernat, G., Ferdinand, C., Heckmann, R., Mitra, T., Mueller, F., Puaut, I., Puschner, P., Staschulat, J., Stenström, P.: The worst-case execution-time problem–overview of methods and survey of tools. ACM Trans. Embed. Comput. Syst. 7(3), 36:1–36:53 (2008)

    Article  Google Scholar 

  36. Younes, H.L.S., Reid, G.: Simmons. Statistical probabilistic model checking with a focus on time-bounded properties. Inf. Comput. 204(9), 1368–1409 (2006)

    Article  MATH  Google Scholar 

  37. Zhang, N., Burns, A., Nicholson, M.: Pipelined processors and worst case execution times. Real-Time Syst. 5(4), 319–343 (1993)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Aalborg University, Aalborg, Denmark

    Anders P. Ravn, Bent Thomsen, Lone Leth & Thomas Bøgholm

  2. Carnegie Mellon University, Silicon Valley, NASA Ames, Mountain View, USA

    Kasper Søe Luckow

Authors
  1. Anders P. Ravn
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Bent Thomsen
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Kasper Søe Luckow
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Lone Leth
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Thomas Bøgholm
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Anders P. Ravn .

Editor information

Editors and Affiliations

  1. Reykjavik University, Reykjavik, Iceland

    Luca Aceto

  2. Aalborg University, Aalborg, Denmark

    Giorgio Bacci

  3. Aalborg University, Aalborg, Denmark

    Giovanni Bacci

  4. Reykjavík University, Reykjavik, Iceland

    Anna Ingólfsdóttir

  5. Inria Campus Beaulieu, Rennes, France

    Axel Legay

  6. Aalborg University, Aalborg, Denmark

    Radu Mardare

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this chapter

Cite this chapter

Ravn, A.P., Thomsen, B., Søe Luckow, K., Leth, L., Bøgholm, T. (2017). Firm Deadline Checking of Safety-Critical Java Applications with Statistical Model Checking. In: Aceto, L., Bacci, G., Bacci, G., Ingólfsdóttir, A., Legay, A., Mardare, R. (eds) Models, Algorithms, Logics and Tools. Lecture Notes in Computer Science(), vol 10460. Springer, Cham. https://doi.org/10.1007/978-3-319-63121-9_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-63121-9_14

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-63120-2

  • Online ISBN: 978-3-319-63121-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation