{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T00:17:20Z","timestamp":1760055440224,"version":"build-2065373602"},"publisher-location":"Cham","reference-count":50,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319568409"},{"type":"electronic","value":"9783319568416"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-56841-6_4","type":"book-chapter","created":{"date-parts":[[2017,4,5]],"date-time":"2017-04-05T13:00:33Z","timestamp":1491397233000},"page":"110-150","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Java in the Safety-Critical Domain"],"prefix":"10.1007","author":[{"given":"Ana","family":"Cavalcanti","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alvaro","family":"Miyazawa","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andy","family":"Wellings","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jim","family":"Woodcock","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shuai","family":"Zhao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,4,6]]},"reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"Aichernig, B., Contract-based Mutation Testing in the Refinement Calculus. In: REFINE 2002. Electronic Notes in Theoretical Computer Science, Invited paper (2002)","DOI":"10.1016\/S1571-0661(05)82561-7"},{"key":"4_CR2","series-title":"Graduate Texts in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-1674-2","volume-title":"Refinement Calculus: A Systematic Introduction","author":"RJR Back","year":"1998","unstructured":"Back, R.J.R., Wright, J.: Refinement Calculus: A Systematic Introduction. Graduate Texts in Computer Science. Springer, New York (1998)"},{"key":"4_CR3","volume-title":"High Integrity Software: The SPARK Approach to Safety and Security","author":"J Barnes","year":"2003","unstructured":"Barnes, J.: High Integrity Software: The SPARK Approach to Safety and Security. Addison-Wesley, Boston (2003)"},{"key":"4_CR4","volume-title":"Formal Specifications and Software Development","author":"D Bjorner","year":"1982","unstructured":"Bjorner, D., Jones, C.B.: Formal Specifications and Software Development. Prentice-Hall, Upper Saddle River (1982)"},{"key":"4_CR5","unstructured":"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)"},{"key":"4_CR6","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1145\/340396.340450","volume":"XIX","author":"A Burns","year":"1999","unstructured":"Burns, A.: The Ravenscar profile. Ada Lett. XIX, 49\u201352 (1999)","journal-title":"Ada Lett."},{"key":"4_CR7","unstructured":"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"},{"issue":"4","key":"4_CR8","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1007\/s00165-010-0170-3","volume":"23","author":"ALC Cavalcanti","year":"2011","unstructured":"Cavalcanti, A.L.C., Clayton, P., O\u2019Halloran, C.: From control law diagrams to Ada via Circus. Form. Asp. Comput. 23(4), 465\u2013512 (2011)","journal-title":"Form. Asp. Comput."},{"issue":"1","key":"4_CR9","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/S0167-6423(97)00015-4","volume":"33","author":"ALC Cavalcanti","year":"1999","unstructured":"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\u201396 (1999)","journal-title":"Sci. Comput. Program."},{"issue":"2\u20133","key":"4_CR10","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/s00165-003-0006-5","volume":"15","author":"ALC Cavalcanti","year":"2003","unstructured":"Cavalcanti, A.L.C., Sampaio, A.C.A., Woodcock, J.C.P.: A refinement strategy for Circus. Form. Asp. Comput. 15(2\u20133), 146\u2013181 (2003)","journal-title":"Form. Asp. Comput."},{"issue":"3","key":"4_CR11","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/s10270-005-0085-2","volume":"4","author":"ALC Cavalcanti","year":"2005","unstructured":"Cavalcanti, A.L.C., Sampaio, A.C.A., Woodcock, J.C.P.: Unifying classes and processes. Softw. Syst. Model. 4(3), 277\u2013296 (2005)","journal-title":"Softw. Syst. Model."},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1145\/2043910.2043915"},{"issue":"3","key":"4_CR13","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/s001650050016","volume":"10","author":"ALC Cavalcanti","year":"1999","unstructured":"Cavalcanti, A.L.C., Woodcock, J.C.P.: ZRC\u2014a refinement calculus for Z. Form. Asp. Comput. 10(3), 267\u2013289 (1999)","journal-title":"Form. Asp. Comput."},{"issue":"5","key":"4_CR14","doi-asserted-by":"publisher","first-page":"614","DOI":"10.1007\/s11241-013-9182-4","volume":"49","author":"ALC Cavalcanti","year":"2013","unstructured":"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\u2013667 (2013)","journal-title":"Real-Time Syst."},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"Corn\u00e9lio, 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)","DOI":"10.1016\/S1571-0661(05)82564-2"},{"key":"4_CR16","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"EW Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded commands, nondeterminacy and the formal derivation of programs. Commun. ACM 18, 453\u2013457 (1975)","journal-title":"Commun. ACM"},{"key":"4_CR17","volume-title":"An Introduction to Formal Methods","author":"AZ Diller","year":"1994","unstructured":"Diller, A.Z.: An Introduction to Formal Methods, 2nd edn. Wiley, Hoboken (1994)","edition":"2"},{"key":"4_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/3-540-36103-0_36","volume-title":"Formal Methods and Software Engineering","author":"AA Duran","year":"2002","unstructured":"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\u2013358. Springer, Heidelberg (2002). doi:10.1007\/3-540-36103-0_36"},{"key":"4_CR19","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/978-0-387-35261-9_29","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"C Fischer","year":"1997","unstructured":"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\u2013438. Chapman & Hall, Boca Raton (1997)"},{"key":"4_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/978-3-540-49676-2_2","volume-title":"ZUM 1998: The Z Formal Specification Notation","author":"C Fischer","year":"1998","unstructured":"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\u201323. Springer, Heidelberg (1998). doi:10.1007\/978-3-540-49676-2_2"},{"key":"4_CR21","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/BF00289507","volume":"1","author":"CAR Hoare","year":"1972","unstructured":"Hoare, C.A.R.: Proof of correctness of data representations. Acta Informatica 1, 271\u2013281 (1972)","journal-title":"Acta Informatica"},{"key":"4_CR22","volume-title":"Communicating Sequential Processes","author":"CAR Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall International, Upper Saddle River (1985)"},{"issue":"6B (special iss","key":"4_CR23","first-page":"1","volume":"14","author":"J Ichbiah","year":"1979","unstructured":"Ichbiah, J.: Rationale for the design of the Ada programming language. ACM SIGPLAN Not. 14(6B (special issue)), 1\u2013261 (1979)","journal-title":"ACM SIGPLAN Not."},{"key":"4_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/3-540-16442-1_14","volume-title":"ESOP 1986","author":"J He","year":"1986","unstructured":"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\u2013196. Springer, Heidelberg (1986). doi:10.1007\/3-540-16442-1_14"},{"issue":"1","key":"4_CR25","first-page":"71","volume":"25","author":"J He","year":"1987","unstructured":"He, J., Hoare, C.A.R., Sanders, J.W.: Prespecification in data refinement. Inf. Process. Lett. 25(1), 71\u201376 (1987)","journal-title":"Inf. Process. Lett."},{"key":"4_CR26","volume-title":"Software Development: A Rigorous Approach","author":"CB Jones","year":"1980","unstructured":"Jones, C.B.: Software Development: A Rigorous Approach. Prentice-Hall, Upper Saddle River (1980)"},{"key":"4_CR27","volume-title":"Systematic Software Development Using VDM","author":"CB Jones","year":"1986","unstructured":"Jones, C.B.: Systematic Software Development Using VDM. Prentice-Hall International, Upper Saddle River (1986)"},{"issue":"6","key":"4_CR28","doi-asserted-by":"publisher","first-page":"1811","DOI":"10.1145\/197320.197383","volume":"16","author":"BH Liskov","year":"1994","unstructured":"Liskov, B.H., Wing, J.M.: A behavioural notion of subtyping. ACM Trans. Program. Lang. Syst. 16(6), 1811\u20131841 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"4_CR29","unstructured":"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"},{"key":"4_CR30","doi-asserted-by":"crossref","unstructured":"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\u2013104. IEEE Computer Society Press (1998)","DOI":"10.1109\/ICSE.1998.671106"},{"key":"4_CR31","unstructured":"Meisels, I.: Software Manual for Windows Z\/EVES Version 2.1. ORA Canada, TR-97-5505-04g (2000)"},{"key":"4_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-319-29473-5_6","volume-title":"Formal Methods: Foundations and Applications","author":"A Miyazawa","year":"2016","unstructured":"Miyazawa, A., Cavalcanti, A.L.C.: Refinement strategies for safety-critical Java. In: Corn\u00e9lio, M.L., Roscoe, B. (eds.) SBMF 2015. LNCS, vol. 9526, pp. 93\u2013109. Springer, Cham (2016). doi:10.1007\/978-3-319-29473-5_6"},{"issue":"6","key":"4_CR33","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/0020-0190(88)90227-X","volume":"29","author":"CC Morgan","year":"1988","unstructured":"Morgan, C.C.: Auxiliary variables in data refinement. Inf. Process. Lett. 29(6), 293\u2013296 (1988)","journal-title":"Inf. Process. Lett."},{"key":"4_CR34","volume-title":"Programming from Specifications","author":"CC Morgan","year":"1994","unstructured":"Morgan, C.C.: Programming from Specifications, 2nd edn. Prentice-Hall, Upper Saddle River (1994)","edition":"2"},{"issue":"6","key":"4_CR35","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1007\/BF00277386","volume":"27","author":"CC Morgan","year":"1990","unstructured":"Morgan, C.C., Gardiner, P.H.B.: Data refinement by calculation. Acta Informatica 27(6), 481\u2013503 (1990)","journal-title":"Acta Informatica"},{"issue":"3","key":"4_CR36","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1016\/0167-6423(87)90011-6","volume":"9","author":"JM Morris","year":"1987","unstructured":"Morris, J.M.: A theoretical basis for stepwise refinement and the programming calculus. Sci. Comput. Program. 9(3), 287\u2013306 (1987)","journal-title":"Sci. Comput. Program."},{"key":"4_CR37","unstructured":"Motor Industry Software Reliability Association Guidelines. Guidelines for Use of the C Language in Critical Systems (2012)"},{"key":"4_CR38","volume-title":"An Introduction to Formal Specification and Z","author":"BF Potter","year":"1996","unstructured":"Potter, B.F., Sinclair, J.E., Till, D.: An Introduction to Formal Specification and Z, 2nd edn. Prentice-Hall, Upper Saddle River (1996)","edition":"2"},{"key":"4_CR39","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1016\/0304-3975(88)90030-8","volume":"58","author":"GM Reed","year":"1988","unstructured":"Reed, G.M., Roscoe, A.W.: A timed model for communicating sequential processes. Theoret. Comput. Sci. 58, 249\u2013261 (1988)","journal-title":"Theoret. Comput. Sci."},{"key":"4_CR40","series-title":"Prentice-Hall Series in Computer Science","volume-title":"The Theory and Practice of Concurrency","author":"AW Roscoe","year":"1998","unstructured":"Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall Series in Computer Science. Prentice-Hall, Upper Saddle River (1998)"},{"key":"4_CR41","series-title":"Texts in Computer Science","volume-title":"Understanding Concurrent Systems","author":"AW Roscoe","year":"2011","unstructured":"Roscoe, A.W.: Understanding Concurrent Systems. Texts in Computer Science. Springer, London (2011)"},{"key":"4_CR42","unstructured":"RTCA\/DO-178C\/ED-12C: Software Considerations in Airborne Systems and Equipment Certification (2011)"},{"key":"4_CR43","series-title":"AMAST Series in Computing","doi-asserted-by":"crossref","DOI":"10.1142\/2870","volume-title":"An Algebraic Approach to Compiler Design","author":"ACA Sampaio","year":"1997","unstructured":"Sampaio, A.C.A.: An Algebraic Approach to Compiler Design. AMAST Series in Computing, vol. 4. World Scientific, Singapore (1997)"},{"key":"4_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"416","DOI":"10.1007\/3-540-45648-1_22","volume-title":"ZB 2002:Formal Specification and Development in Z and B","author":"S Schneider","year":"2002","unstructured":"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\u2013435. Springer, Heidelberg (2002). doi:10.1007\/3-540-45648-1_22"},{"issue":"2","key":"4_CR45","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/s00165-009-0119-6","volume":"22","author":"A Sherif","year":"2010","unstructured":"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\u2013191 (2010)","journal-title":"Form. Asp. Comput."},{"issue":"2","key":"4_CR46","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1006\/inco.1996.2613","volume":"132","author":"M Tofte","year":"1997","unstructured":"Tofte, M., Talpin, J.-P.: Region-based memory management. Inf. Comput. 132(2), 109\u2013176 (1997)","journal-title":"Inf. Comput."},{"key":"4_CR47","volume-title":"Concurrent and Real-Time Programming in Java","author":"A Wellings","year":"2004","unstructured":"Wellings, A.: Concurrent and Real-Time Programming in Java. Wiley, Hoboken (2004)"},{"key":"4_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/3-540-45614-7_28","volume-title":"FME 2002:Formal Methods\u2014Getting IT Right","author":"L Wildman","year":"2002","unstructured":"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\u2013510. Springer, Heidelberg (2002). doi:10.1007\/3-540-45614-7_28"},{"key":"4_CR49","volume-title":"Using Z-Specification, Refinement, and Proof","author":"JCP Woodcock","year":"1996","unstructured":"Woodcock, J.C.P., Davies, J.: Using Z-Specification, Refinement, and Proof. Prentice-Hall, Upper Saddle River (1996)"},{"issue":"7","key":"4_CR50","doi-asserted-by":"publisher","first-page":"1046","DOI":"10.1093\/comjnl\/bxt060","volume":"57","author":"F Zeyda","year":"2014","unstructured":"Zeyda, F., Lalkhumsanga, L., Cavalcanti, A.L.C., Wellings, A.: Circus models for safety-critical Java programs. Comput. J. 57(7), 1046\u20131091 (2014)","journal-title":"Comput. J."}],"container-title":["Lecture Notes in Computer Science","Engineering Trustworthy Software Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-56841-6_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T05:23:29Z","timestamp":1759987409000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-56841-6_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319568409","9783319568416"],"references-count":50,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-56841-6_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"6 April 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SETSS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"School on Engineering Trustworthy Software Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Chongqing","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2016","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 March 2016","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 April 2016","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"setss2016","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}