Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Alan Turing: Founder of Computer Science Kapitel lesen Erstes Kapitel lesen

2017 | OriginalPaper | Buchkapitel

Java in the Safety-Critical Domain

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

Erschienen in: Engineering Trustworthy Software Systems

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren
Vorheriges Kapitel Reasoned Modelling with Event-B
Nächstes Kapitel Runtime Verification for Linear-Time Temporal Logic
Literatur
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.
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 CrossRef
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
Metadaten
Titel
Java in the Safety-Critical Domain
verfasst von
Ana Cavalcanti
Alvaro Miyazawa
Andy Wellings
Jim Woodcock
Shuai Zhao
Copyright-Jahr
2017
Buch
Engineering Trustworthy Software Systems

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

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

Copyright-Jahr: 2017

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