Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Alan Turing: Founder of Computer Science Read chapter Read first chapter

2017 | OriginalPaper | Chapter

Java in the Safety-Critical Domain

Authors : Ana Cavalcanti, Alvaro Miyazawa, Andy Wellings, Jim Woodcock, Shuai Zhao

Published in: Engineering Trustworthy Software Systems

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

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 https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-56841-6_4/448793_1_En_4_IEq1_HTML.gif 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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter Reasoned Modelling with Event-B
next chapter Runtime Verification for Linear-Time Temporal Logic
Literature
1.
Aichernig, B., Contract-based Mutation Testing in the Refinement Calculus. In: REFINE 2002. Electronic Notes in Theoretical Computer Science, Invited paper (2002)
2.
Back, R.J.R., Wright, J.: Refinement Calculus: A Systematic Introduction. Graduate Texts in Computer Science. Springer, New York (1998)CrossRefMATH
3.
Barnes, J.: High Integrity Software: The SPARK Approach to Safety and Security. Addison-Wesley, Boston (2003)
4.
Bjorner, D., Jones, C.B.: Formal Specifications and Software Development. Prentice-Hall, Upper Saddle River (1982)MATH
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)
6.
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
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)CrossRefMATH
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)MathSciNetCrossRefMATH
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)CrossRefMATH
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)CrossRef
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)
13.
Cavalcanti, A.L.C., Woodcock, J.C.P.: ZRC—a refinement calculus for Z. Form. Asp. Comput. 10(3), 267–289 (1999)CrossRefMATH
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)CrossRefMATH
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)
16.
17.
Diller, A.Z.: An Introduction to Formal Methods, 2nd edn. Wiley, Hoboken (1994)MATH
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 CrossRef
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)CrossRef
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
21.
Hoare, C.A.R.: Proof of correctness of data representations. Acta Informatica 1, 271–281 (1972)CrossRefMATH
22.
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall International, Upper Saddle River (1985)MATH
23.
Ichbiah, J.: Rationale for the design of the Ada programming language. ACM SIGPLAN Not. 14(6B (special issue)), 1–261 (1979)
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
25.
He, J., Hoare, C.A.R., Sanders, J.W.: Prespecification in data refinement. Inf. Process. Lett. 25(1), 71–76 (1987)MathSciNetMATH
26.
Jones, C.B.: Software Development: A Rigorous Approach. Prentice-Hall, Upper Saddle River (1980)MATH
27.
Jones, C.B.: Systematic Software Development Using VDM. Prentice-Hall International, Upper Saddle River (1986)MATH
28.
Liskov, B.H., Wing, J.M.: A behavioural notion of subtyping. ACM Trans. Program. Lang. Syst. 16(6), 1811–1841 (1994)CrossRef
29.
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)
31.
Meisels, I.: Software Manual for Windows Z/EVES Version 2.1. ORA Canada, TR-97-5505-04g (2000)
32.
33.
34.
Morgan, C.C.: Programming from Specifications, 2nd edn. Prentice-Hall, Upper Saddle River (1994)MATH
35.
36.
Morris, J.M.: A theoretical basis for stepwise refinement and the programming calculus. Sci. Comput. Program. 9(3), 287–306 (1987)MathSciNetCrossRefMATH
37.
Motor Industry Software Reliability Association Guidelines. Guidelines for Use of the C Language in Critical Systems (2012)
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
39.
40.
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall Series in Computer Science. Prentice-Hall, Upper Saddle River (1998)
41.
Roscoe, A.W.: Understanding Concurrent Systems. Texts in Computer Science. Springer, London (2011)MATH
42.
RTCA/DO-178C/ED-12C: Software Considerations in Airborne Systems and Equipment Certification (2011)
43.
Sampaio, A.C.A.: An Algebraic Approach to Compiler Design. AMAST Series in Computing, vol. 4. World Scientific, Singapore (1997)MATH
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 CrossRef
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)CrossRefMATH
46.
47.
Wellings, A.: Concurrent and Real-Time Programming in Java. Wiley, Hoboken (2004)
48.
49.
Woodcock, J.C.P., Davies, J.: Using Z-Specification, Refinement, and Proof. Prentice-Hall, Upper Saddle River (1996)MATH
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)CrossRef
Metadata
Title
Java in the Safety-Critical Domain
Authors
Ana Cavalcanti
Alvaro Miyazawa
Andy Wellings
Jim Woodcock
Shuai Zhao
Copyright Year
2017
Book
Engineering Trustworthy Software Systems

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

Electronic ISBN: 978-3-319-56841-6

Copyright Year: 2017

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

Premium Partner

    Image Credits