Skip to main content
SpringerLink
Log in

Java in the Safety-Critical Domain

  • Chapter
  • First Online:
Engineering Trustworthy Software Systems (SETSS 2016)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10215))

Included in the following conference series:

Abstract

Safety-Critical Java (SCJ) is an Open Group standard that defines a novel version of Java suitable for programming systems with various levels of criticality. SCJ enables real-time programming and certification of safety-critical applications. This tutorial presents SCJ and an associated verification technique to prove correctness of programs based on refinement. For modelling, we use the family of notations, which combine Z, CSP, Timed CSP, and object orientation. The technique caters for the specification of functional and timing requirements, and establishes the correctness of designs based on architectures that use the structure of missions and event handlers of SCJ. It also considers the integrated refinement of value-based specifications into class-based designs using SCJ scoped memory areas. As an example, we use an SCJ implementation of a widely used leadership-election protocol.

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

Access this chapter

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

Institutional subscriptions

References

  1. Aichernig, B., Contract-based Mutation Testing in the Refinement Calculus. In: REFINE 2002. Electronic Notes in Theoretical Computer Science, Invited paper (2002)

    Google Scholar 

  2. Back, R.J.R., Wright, J.: Refinement Calculus: A Systematic Introduction. Graduate Texts in Computer Science. Springer, New York (1998)

    Book  MATH  Google Scholar 

  3. Barnes, J.: High Integrity Software: The SPARK Approach to Safety and Security. Addison-Wesley, Boston (2003)

    Google Scholar 

  4. Bjorner, D., Jones, C.B.: Formal Specifications and Software Development. Prentice-Hall, Upper Saddle River (1982)

    MATH  Google Scholar 

  5. Bolognesi, T.: On state-oriented versus object-oriented thinking in formal behavioural specifications. Technical report -TR-20, ISTI-Istituto di Scienza e Tecnologie della Informazione Alessandro Faedo (2003)

    Google Scholar 

  6. Burns, A.: The Ravenscar profile. Ada Lett. XIX, 49–52 (1999)

    Article  Google Scholar 

  7. Cavalcanti, A.L.C.: A refinement calculus for Z. Ph.D. thesis, Oxford University Computing Laboratory, Oxford, UK (1997). Technical Monograph TM-PRG-123, ISBN 00902928-97-X

    Google Scholar 

  8. Cavalcanti, A.L.C., Clayton, P., O’Halloran, C.: From control law diagrams to Ada via Circus. Form. Asp. Comput. 23(4), 465–512 (2011)

    Article  MATH  Google Scholar 

  9. Cavalcanti, A.L.C., Sampaio, A.C.A., Woodcock, J.C.P.: An inconsistency in procedures, parameters, and substitution the refinement calculus. Sci. Comput. Program. 33(1), 87–96 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  10. Cavalcanti, A.L.C., Sampaio, A.C.A., Woodcock, J.C.P.: A refinement strategy for Circus. Form. Asp. Comput. 15(2–3), 146–181 (2003)

    Article  MATH  Google Scholar 

  11. Cavalcanti, A.L.C., Sampaio, A.C.A., Woodcock, J.C.P.: Unifying classes and processes. Softw. Syst. Model. 4(3), 277–296 (2005)

    Article  Google Scholar 

  12. Cavalcanti, A.L.C., Wellings, A., Woodcock, J.C.P., Wei, K., Zeyda, F.: Safety-critical Java in Circus. In: Ravn, A.P. (ed.) 9th Workshop on Java Technologies for Real-Time and Embedded System. ACM Digital Library. ACM (2011)

    Google Scholar 

  13. Cavalcanti, A.L.C., Woodcock, J.C.P.: ZRC—a refinement calculus for Z. Form. Asp. Comput. 10(3), 267–289 (1999)

    Article  MATH  Google Scholar 

  14. Cavalcanti, A.L.C., Zeyda, F., Wellings, A., Woodcock, J.C.P., Wei, K.: Safety-critical Java programs from Circus models. Real-Time Syst. 49(5), 614–667 (2013)

    Article  MATH  Google Scholar 

  15. Cornélio, M.L., Cavalcanti, A.L.C., Sampaio, A.C.A.: Refactoring by transformation. In: Derrick, J., Boiten, E., Woodcock, J.C.P., Wright, J. (eds.) REFINE 2002. Electronic Notes in Theoretical Computer Science, Invited paper, vol. 70. Elsevier (2002)

    Google Scholar 

  16. Dijkstra, E.W.: Guarded commands, nondeterminacy and the formal derivation of programs. Commun. ACM 18, 453–457 (1975)

    Article  MathSciNet  MATH  Google Scholar 

  17. Diller, A.Z.: An Introduction to Formal Methods, 2nd edn. Wiley, Hoboken (1994)

    MATH  Google Scholar 

  18. Duran, A.A., Cavalcanti, A.C.A., Sampaio, A.L.C.: Refinement algebra for formal bytecode generation. In: George, C., Miao, H. (eds.) ICFEM 2002. LNCS, vol. 2495, pp. 347–358. Springer, Heidelberg (2002). doi:10.1007/3-540-36103-0_36

    Chapter  Google Scholar 

  19. Fischer, C.: CSP-OZ: a combination of object-Z and CSP. In: Bowman, H., Derrick, J. (eds.) Formal Methods for Open Object-Based Distributed Systems, vol. 2, pp. 423–438. Chapman & Hall, Boca Raton (1997)

    Chapter  Google Scholar 

  20. Fischer, C.: How to combine Z with a process algebra. In: Bowen, J.P., Fett, A., Hinchey, M.G. (eds.) ZUM 1998. LNCS, vol. 1493, pp. 5–23. Springer, Heidelberg (1998). doi:10.1007/978-3-540-49676-2_2

    Google Scholar 

  21. Hoare, C.A.R.: Proof of correctness of data representations. Acta Informatica 1, 271–281 (1972)

    Article  MATH  Google Scholar 

  22. Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall International, Upper Saddle River (1985)

    MATH  Google Scholar 

  23. Ichbiah, J.: Rationale for the design of the Ada programming language. ACM SIGPLAN Not. 14(6B (special issue)), 1–261 (1979)

    Google Scholar 

  24. He, J., Hoare, C.A.R., Sanders, J.W.: Data refinement refined resume. In: Robinet, B., Wilhelm, R. (eds.) ESOP 1986. LNCS, vol. 213, pp. 187–196. Springer, Heidelberg (1986). doi:10.1007/3-540-16442-1_14

    Google Scholar 

  25. He, J., Hoare, C.A.R., Sanders, J.W.: Prespecification in data refinement. Inf. Process. Lett. 25(1), 71–76 (1987)

    MathSciNet  MATH  Google Scholar 

  26. Jones, C.B.: Software Development: A Rigorous Approach. Prentice-Hall, Upper Saddle River (1980)

    MATH  Google Scholar 

  27. Jones, C.B.: Systematic Software Development Using VDM. Prentice-Hall International, Upper Saddle River (1986)

    MATH  Google Scholar 

  28. Liskov, B.H., Wing, J.M.: A behavioural notion of subtyping. ACM Trans. Program. Lang. Syst. 16(6), 1811–1841 (1994)

    Article  Google Scholar 

  29. 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 Specification, First Release 0.76. The Open Group, UK (2010). jcp.org/aboutJava/communityprocess/edr/jsr302/index.html

  30. Mahony, B.P., Dong, J.S.: Blending object-Z and timed CSP: an introduction to TCOZ. In: 20th International Conference on Software Engineering (ICSE 1998), pp. 95–104. IEEE Computer Society Press (1998)

    Google Scholar 

  31. Meisels, I.: Software Manual for Windows Z/EVES Version 2.1. ORA Canada, TR-97-5505-04g (2000)

    Google Scholar 

  32. Miyazawa, A., Cavalcanti, A.L.C.: Refinement strategies for safety-critical Java. In: Cornélio, M.L., Roscoe, B. (eds.) SBMF 2015. LNCS, vol. 9526, pp. 93–109. Springer, Cham (2016). doi:10.1007/978-3-319-29473-5_6

    Chapter  Google Scholar 

  33. Morgan, C.C.: Auxiliary variables in data refinement. Inf. Process. Lett. 29(6), 293–296 (1988)

    Article  MathSciNet  MATH  Google Scholar 

  34. Morgan, C.C.: Programming from Specifications, 2nd edn. Prentice-Hall, Upper Saddle River (1994)

    MATH  Google Scholar 

  35. Morgan, C.C., Gardiner, P.H.B.: Data refinement by calculation. Acta Informatica 27(6), 481–503 (1990)

    Article  MathSciNet  MATH  Google Scholar 

  36. Morris, J.M.: A theoretical basis for stepwise refinement and the programming calculus. Sci. Comput. Program. 9(3), 287–306 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  37. Motor Industry Software Reliability Association Guidelines. Guidelines for Use of the C Language in Critical Systems (2012)

    Google Scholar 

  38. Potter, B.F., Sinclair, J.E., Till, D.: An Introduction to Formal Specification and Z, 2nd edn. Prentice-Hall, Upper Saddle River (1996)

    MATH  Google Scholar 

  39. Reed, G.M., Roscoe, A.W.: A timed model for communicating sequential processes. Theoret. Comput. Sci. 58, 249–261 (1988)

    Article  MathSciNet  MATH  Google Scholar 

  40. Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall Series in Computer Science. Prentice-Hall, Upper Saddle River (1998)

    Google Scholar 

  41. Roscoe, A.W.: Understanding Concurrent Systems. Texts in Computer Science. Springer, London (2011)

    MATH  Google Scholar 

  42. RTCA/DO-178C/ED-12C: Software Considerations in Airborne Systems and Equipment Certification (2011)

    Google Scholar 

  43. Sampaio, A.C.A.: An Algebraic Approach to Compiler Design. AMAST Series in Computing, vol. 4. World Scientific, Singapore (1997)

    MATH  Google Scholar 

  44. Schneider, S., Treharne, H.: Communicating B machines. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) ZB 2002. LNCS, vol. 2272, pp. 416–435. Springer, Heidelberg (2002). doi:10.1007/3-540-45648-1_22

    Chapter  Google Scholar 

  45. Sherif, A., Cavalcanti, A.L.C., He, J., Sampaio, A.C.A.: A process algebraic framework for specification and validation of real-time systems. Form. Asp. Comput. 22(2), 153–191 (2010)

    Article  MATH  Google Scholar 

  46. Tofte, M., Talpin, J.-P.: Region-based memory management. Inf. Comput. 132(2), 109–176 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  47. Wellings, A.: Concurrent and Real-Time Programming in Java. Wiley, Hoboken (2004)

    Google Scholar 

  48. Wildman, L.: A formal basis for a program compilation proof tool. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 491–510. Springer, Heidelberg (2002). doi:10.1007/3-540-45614-7_28

    Chapter  Google Scholar 

  49. Woodcock, J.C.P., Davies, J.: Using Z-Specification, Refinement, and Proof. Prentice-Hall, Upper Saddle River (1996)

    MATH  Google Scholar 

  50. Zeyda, F., Lalkhumsanga, L., Cavalcanti, A.L.C., Wellings, A.: Circus models for safety-critical Java programs. Comput. J. 57(7), 1046–1091 (2014)

    Article  Google Scholar 

Download references

Acknowledgments

This work is funded by EPSRC grant EP/H017461/1. No primary data arises from the work reported here. We have benefitted from discussions with Frank Zeyda in the development of our case study.

Author information

Authors and Affiliations

  1. Department of Computer Science, University of York, York, UK

    Ana Cavalcanti, Alvaro Miyazawa, Andy Wellings, Jim Woodcock & Shuai Zhao

Authors
  1. Ana Cavalcanti
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Alvaro Miyazawa
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Andy Wellings
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Jim Woodcock
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Shuai Zhao
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Ana Cavalcanti .

Editor information

Editors and Affiliations

  1. London South Bank University, London, United Kingdom

    Jonathan P. Bowen

  2. Southwest University, Chongqing, China

    Zhiming Liu

  3. Southwest University, Chongqing, China

    Zili Zhang

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this chapter

Cite this chapter

Cavalcanti, A., Miyazawa, A., Wellings, A., Woodcock, J., Zhao, S. (2017). Java in the Safety-Critical Domain. In: Bowen, J., Liu, Z., Zhang, Z. (eds) Engineering Trustworthy Software Systems. SETSS 2016. Lecture Notes in Computer Science(), vol 10215. Springer, Cham. https://doi.org/10.1007/978-3-319-56841-6_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-56841-6_4

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-56840-9

  • Online ISBN: 978-3-319-56841-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation