Advertisement

Algebraic Compilation of Safety-Critical Java Bytecode

  • James BaxterEmail author
  • Ana Cavalcanti
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10510)

Abstract

Safety-Critical Java (SCJ) is a version of Java that facilitates the development of certifiable programs, and requires a specialised virtual machine (SCJVM). In spite of the nature of the applications for which SCJ is designed, none of the SCJVMs are verified. In this paper, we contribute a formal specification of a bytecode interpreter for SCJ and an algebraic compilation strategy from Java bytecode to C. For the target C code, we adopt the compilation approach for icecap, the only SCJVM that is open source and up-to-date with the SCJ standard. Our work enables either prototyping of a verified compiler, or full verification of icecap or any other SCJVM.

Notes

Acknowledgements

The authors gratefully acknowledge useful feedback from Augusto Sampaio on the application of the algebraic approach. We also thank Andy Wellings for his advice on SCJ and Leo Freitas for his help with the use of Z/EVES and understanding of icecap. This work is supported by EPSRC studentship 1511661 and EPSRC grant EP/H017461/1.

References

  1. 1.
    Armbruster, A., Baker, J., Cunei, A., et al.: A real-time Java virtual machine with applications in avionics. ACM Trans. Embed. Comput. Syst. 7(1), 5:1–5:49 (2007)CrossRefGoogle Scholar
  2. 2.
    Baxter, J.: An Approach to verification of Safety-Critical Java Virtual Machines with Ahead-of-time compilation. Technical report, University of York (2017). www-users.cs.york.ac.uk/~jeb531/2017report.pdf
  3. 3.
    Baxter, J., Cavalcanti, A., Wellings, A., Freitas, L.: Safety-critical Java virtual machine services. In: JTRES 2015, pp. 7:1–7:10. ACM (2015)Google Scholar
  4. 4.
    Blazy, S., Dargaye, Z., Leroy, X.: Formal verification of a C compiler front-end. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 460–475. Springer, Heidelberg (2006). doi: 10.1007/11813040_31 CrossRefGoogle Scholar
  5. 5.
    Cavalcanti, A., Wellings, A., Woodcock, J., Wei, K., Zeyda, F.: Safety-critical Java in circus. In: JTRES 2011, pp. 20–29. ACM (2011)Google Scholar
  6. 6.
    Cavalcanti, A., Zeyda, F., Wellings, A., Woodcock, J., Wei, K.: Safety-critical Java programs from Circus models. Real-Time Syst. 49(5), 614–667 (2013)CrossRefzbMATHGoogle Scholar
  7. 7.
    Clavel, M., Durán, F., Eker, S., Lincoln, P., Martı-Oliet, N., Meseguer, J., Quesada, J.F.: Maude: specification and programming in rewriting logic. Theoret. Comput. Sci. 285(2), 187–243 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18(8), 453–457 (1975)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Duran, A.: An Algebraic Approach to the Design of Compilers for Object-Oriented Languages. Ph.D. thesis, Universidade Federal de Pernambuco (2005)Google Scholar
  10. 10.
    Freitas, L., Baxter, J., Cavalcanti, A., Wellings, A.: Modelling and verifying a priority scheduler for an SCJ runtime environment. In: Ábrahám, E., Huisman, M. (eds.) IFM 2016. LNCS, vol. 9681, pp. 63–78. Springer, Cham (2016). doi: 10.1007/978-3-319-33693-0_5 CrossRefGoogle Scholar
  11. 11.
    Kalibera, T., Parizek, P., Malohlava, M., Schoeberl, M.: Exhaustive testing of safety critical java. In: JTRES 2010, pp. 164–174. ACM (2010)Google Scholar
  12. 12.
    Klein, G., Nipkow, T.: A machine-checked model for a Java-like language, virtual machine, and compiler. ACM Trans. Program. Lang. Syst. 28(4), 619–695 (2006)CrossRefGoogle Scholar
  13. 13.
    Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009)CrossRefGoogle Scholar
  14. 14.
    Leroy, X.: A formally verified compiler back-end. J. Autom. Reason. 43(4), 363–446 (2009)MathSciNetCrossRefzbMATHGoogle Scholar
  15. 15.
    Lochbihler, A.: Verifying a compiler for Java threads. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 427–447. Springer, Heidelberg (2010). doi: 10.1007/978-3-642-11957-6_23 CrossRefGoogle Scholar
  16. 16.
    Locke, D., et al.: Safety-Critical Java Technology Specification. https://jcp.org/aboutJava/communityprocess/edr/jsr302/index2.html
  17. 17.
    Marriott, C.: Checking Memory Safety of Level 1 Safety-Critical Java Programs using Static-Analysis without Annotations. Ph.D. thesis, University of York (2014)Google Scholar
  18. 18.
    Motor Industry Software Reliability Association Guidelines: Guidelines for Use of the C Language in Critical Systems (2012)Google Scholar
  19. 19.
    Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)zbMATHGoogle Scholar
  20. 20.
    Oliveira, M., Cavalcanti, A., Woodcock, J.: A UTP semantics for circus. Formal Aspects Comput. 21(1–2), 3–32 (2009)CrossRefzbMATHGoogle Scholar
  21. 21.
    Perna, J.: A verified compiler for Handel-C. Ph.D. thesis, University of York (2010)Google Scholar
  22. 22.
    Pizlo, F., Ziarek, L., Vitek, J.: Real time Java on resource-constrained platforms with Fiji VM. In: JTRES 2009, pp. 110–119. ACM (2009)Google Scholar
  23. 23.
    Proebsting, T.A., Townsend, G., Bridges, P., et al.: Toba: Java for applications a way ahead of time (wat) compiler. In: Proceedings of the 3rd Conference on Object-Oriented Technologies and Systems (1997)Google Scholar
  24. 24.
    Roscoe, A.W.: Understanding Concurrent Systems. Texts in Computer Science. Springer, London (2011)zbMATHGoogle Scholar
  25. 25.
    Sampaio, A.: An Algebraic Approach to Compiler Design. World Scientific, Singapore (1997)CrossRefzbMATHGoogle Scholar
  26. 26.
    Sawadpong, P., Allen, E.B., Williams, B.J.: Exception handling defects: an empirical study. In: HASE 2012, pp. 90–97. IEEE (2012)Google Scholar
  27. 27.
    Søndergaard, H., Korsholm, S.E., Ravn, A.P.: Safety-critical Java for low-end embedded platforms. In: JTRES 2012, pp. 44–53. ACM (2012)Google Scholar
  28. 28.
    Stärk, R., Schmid, J., Börger, E.: Java and the Java Virtual Machine. Springer, Berlin (2001)CrossRefzbMATHGoogle Scholar
  29. 29.
    Strecker, M.: Formal verification of a Java compiler in isabelle. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 63–77. Springer, Heidelberg (2002). doi: 10.1007/3-540-45620-1_5 CrossRefGoogle Scholar
  30. 30.
    Varma, A., Bhattacharyya, S.S.: Java-through-C compilation: an enabling technology for Java in embedded systems. In: Proceedings of the Conference on Design, Automation and Test in Europe, vol. 3, p. 30161. IEEE Computer Society (2004)Google Scholar
  31. 31.
    Woodcock, J., Davies, J.: Using Z: Specification, Refinement, and Proof. Prentice-Hall Inc., Upper Saddle River (1996)zbMATHGoogle Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  1. 1.Department of Computer ScienceUniversity of YorkYorkUK

Personalised recommendations