Skip to main content
SpringerLink
Log in

A Formal Model of the Safety-Critical Java Level 2 Paradigm

  • Conference paper
  • First Online:
Integrated Formal Methods (IFM 2016)

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

Included in the following conference series:

Abstract

Safety-Critical Java (SCJ) introduces a new programming paradigm for applications that must be certified. The SCJ specification (JSR 302) is an Open Group Standard, but it does not include verification techniques. Previous work has addressed verification for SCJ Level 1 programs. We support the much more complex SCJ Level 2 programs, which allows the programming of highly concurrent multi-processor applications with Java threads, and wait and notify mechanisms. We present a formal model of SCJ Level 2 that captures the state and behaviour of both SCJ programs and the SCJ API. This is the first formal semantics of the SCJ Level 2 paradigm and is an essential ingredient in the development of refinement-based reasoning techniques for SCJ Level 2 programs. We show how our models can be used to prove properties of the SCJ API and applications.

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 69.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 89.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

Notes

  1. 1.

    TightRope can be found at www.cs.york.ac.uk/circus/hijac/tools.html.

References

  1. Bogdanas, D., Roşu, G.: K-Java: a complete semantics of Java. SIGPLAN Not. 50(1), 445–456 (2015)

    Article  Google Scholar 

  2. Cavalcanti, A., Sampaio, A., Woodcock, J.: Unifying classes and processes. Softw. Syst. Model. 4(3), 277–296 (2005). http://dx.doi.org/10.1007/s10270-005-0085-2

    Article  Google Scholar 

  3. Cavalcanti, A., Wellings, A., Woodcock, J., Wei, K., Zeyda, F.: Safety-critical Java in circus. In: Proceedings of the 9th International Workshop on Java Technologies for Real-Time and Embedded Systems, JTRES 2011, pp. 20–29. ACM, New York, NY, USA (2011). http://doi.acm.org/10.1145/2043910.2043915

  4. EUROCAE and RTCA: Software Considerations in Airborne Systems and Equipment Certification. Norm ED-12C, EUROCAE (2012)

    Google Scholar 

  5. Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.: Failures Divergences Refinement (FDR) Version 3 (2013). www.cs.ox.ac.uk/projects/fdr/

  6. Haddad, G., Hussain, F., Leavens, G.T.: The design of SafeJML, a specification language for SCJ with support for WCET specification. In: Proceedings of the 8th International Workshop on Java Technologies for Real-Time and Embedded Systems, JTRES 2010, pp. 155–163. ACM, New York, NY, USA (2010). http://doi.acm.org/10.1145/1850771.1850793

  7. Havelund, K., Pressburger, T.: Model checking JAVA programs using JAVA PathFinder. Int. J. Softw. Tools Technol. Transf. 2(4), 366–381 (2000). http://dx.doi.org/10.1007/s100090050043

    Article  MATH  Google Scholar 

  8. Hoare, C.A.R.: Communicating sequential processes (2004). www.usingcsp.com/cspbook.pdf

  9. IceLab. www.icelab.dk/index.html

  10. Kalibera, T., Parizek, P., Malohlava, M., Schoeberl, M.: Exhaustive testing of safety-critical Java. In: Proceedings of the 8th International Workshop on Java Technologies for Real-Time and Embedded Systems, JTRES 2010, pp. 164–174. ACM, New York, NY, USA (2010). http://doi.acm.org/10.1145/1850771.1850794

  11. Luckcuck, M.: hiJaC Case Studies (2016). www.cs.york.ac.uk/circus/hijac/case.html. Accessed 14 Jan 2016

  12. Luckcuck, M.: Safety-Critical Java Level 2 Framework Model (2016). www.cs.york.ac.uk/circus/publications/techreports/reports/SCJLevel2Framework.pdf

  13. Luckcuck, M., Wellings, A., Cavalcanti, A.: Safety-Critical Java: Level 2 in Practice (submitted)

    Google Scholar 

  14. Morgan, C.: Programming from Specifications. Prentice-Hall, Inc., USA (1990)

    MATH  Google Scholar 

  15. Schoeberl, M.: A Java processor architecture for embedded real-time systems. J. Syst. Architect. 54(1–2), 265–286 (2008). www.sciencedirect.com/science/article/pii/S1383762107000963

    Article  Google Scholar 

  16. Sherif, A., Cavalcanti, A., Jifeng, H., Sampaio, A.: A process algebraic framework for specification and validation of real-time systems. Formal Aspects Comput. 22(2), 153–191 (2009)

    Article  MATH  Google Scholar 

  17. Søndergaard, H., Korsholm, S.E., Ravn, A.P.: Safety-critical Java for low-end embedded platforms. In: Proceedings of the 10th International Workshop on Java Technologies for Real-Time and Embedded Systems, JTRES 2012, pp. 44–53. ACM, New York, NY, USA (2012)

    Google Scholar 

  18. Spivey, J.M.: The Z Notation: A Reference Manual. International Series in Computer Science. Prentice-Hall, Inc. Upper Saddle River (1992)

    Google Scholar 

  19. Tang, D., Plsek, A., Vitek, J.: Static checking of safety critical Java annotations. In: Proceedings of the 8th International Workshop on Java Technologies for Real-Time and Embedded Systems, pp. 148–154. ACM, Prague, Czech Republic (2010)

    Google Scholar 

  20. The Open Group: Safety-critical Java technology specification V0.100. Technical report, The Open Group, 27 December 2014. http://jcp.org/en/jsr/detail?id=302

  21. The Real-Time for Java Expert Group: Real-Time Specification for Java Language Specification (2005). www.timesys.com/java/

  22. Thomsen, B., Luckow, K.S., Leth, L., Bøgholm, T.: From safety critical java programs to timed process models. In: Burrows, M., et al. (eds.) Degano Festschrift. LNCS, vol. 9465, pp. 319–338. Springer, Heidelberg (2015). doi:10.1007/978-3-319-25527-9_21

    Chapter  Google Scholar 

  23. Wellings, A., Luckcuck, M., Cavalcanti, A.: Safety-critical Java level 2: motivations, example applications and issues. In: Proceedings of the 11th International Workshop on Java Technologies for Real-time and Embedded Systems, JTRES 2013, pp. 48–57. ACM, New York, NY, USA (2013). http://doi.acm.org/10.1145/2512989.2512991

  24. Woodcock, J., Cavalcanti, A.: The semantics of \(Circus\). In: Bert, D., Bowen, J.P., C. Henson, M., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, pp. 184–203. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  25. Zeyda, F., Lalkhumsanga, L., Cavalcanti, A., Wellings, A.: Circus models for safety-critical Java programs. Comput. J. 57, 1046–1091 (2013). http://comjnl.oxfordjournals.org/content/early/2013/07/02/comjnl.bxt060.abstract

    Article  MATH  Google Scholar 

Download references

Acknowledgements

This research reported in this paper is funded by the UK EPSRC under grant EP/H017461/1. No new primary data was produced during this work. One of the authors is a member of the SCJ Expert Group; we would like to thank the other members of the Expert Group. We would also like to thank Frank Zeyda, Alan Burns, and Thomas Gibson-Robinson for their very helpful suggestions.

Author information

Authors and Affiliations

  1. Department of Computer Science, University of York, York, YO10 5GH, UK

    Matt Luckcuck, Ana Cavalcanti & Andy Wellings

Authors
  1. Matt Luckcuck
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ana Cavalcanti
    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

Corresponding author

Correspondence to Matt Luckcuck .

Editor information

Editors and Affiliations

  1. RWTH Aachen University, Aachen, Germany

    Erika Ábrahám

  2. University of Twente, Enschede, Overijssel, The Netherlands

    Marieke Huisman

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Luckcuck, M., Cavalcanti, A., Wellings, A. (2016). A Formal Model of the Safety-Critical Java Level 2 Paradigm. In: Ábrahám, E., Huisman, M. (eds) Integrated Formal Methods. IFM 2016. Lecture Notes in Computer Science(), vol 9681. Springer, Cham. https://doi.org/10.1007/978-3-319-33693-0_15

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-33693-0_15

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-33692-3

  • Online ISBN: 978-3-319-33693-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation