{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:20:48Z","timestamp":1740097248596,"version":"3.37.3"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319336923"},{"type":"electronic","value":"9783319336930"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-33693-0_15","type":"book-chapter","created":{"date-parts":[[2016,5,24]],"date-time":"2016-05-24T01:35:47Z","timestamp":1464053747000},"page":"226-241","source":"Crossref","is-referenced-by-count":1,"title":["A Formal Model of the Safety-Critical Java Level 2 Paradigm"],"prefix":"10.1007","author":[{"given":"Matt","family":"Luckcuck","sequence":"first","affiliation":[]},{"given":"Ana","family":"Cavalcanti","sequence":"additional","affiliation":[]},{"given":"Andy","family":"Wellings","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,5,24]]},"reference":[{"issue":"1","key":"15_CR1","doi-asserted-by":"crossref","first-page":"445","DOI":"10.1145\/2775051.2676982","volume":"50","author":"D Bogdanas","year":"2015","unstructured":"Bogdanas, D., Ro\u015fu, G.: K-Java: a complete semantics of Java. SIGPLAN Not. 50(1), 445\u2013456 (2015)","journal-title":"SIGPLAN Not."},{"issue":"3","key":"15_CR2","doi-asserted-by":"crossref","first-page":"277","DOI":"10.1007\/s10270-005-0085-2","volume":"4","author":"A Cavalcanti","year":"2005","unstructured":"Cavalcanti, A., Sampaio, A., Woodcock, J.: Unifying classes and processes. Softw. Syst. Model. 4(3), 277\u2013296 (2005). http:\/\/dx.doi.org\/10.1007\/s10270-005-0085-2","journal-title":"Softw. Syst. Model."},{"key":"15_CR3","doi-asserted-by":"crossref","unstructured":"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\u201329. ACM, New York, NY, USA (2011). http:\/\/doi.acm.org\/10.1145\/2043910.2043915","DOI":"10.1145\/2043910.2043915"},{"key":"15_CR4","unstructured":"EUROCAE and RTCA: Software Considerations in Airborne Systems and Equipment Certification. Norm ED-12C, EUROCAE (2012)"},{"key":"15_CR5","unstructured":"Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.: Failures Divergences Refinement (FDR) Version 3 (2013). www.cs.ox.ac.uk\/projects\/fdr\/"},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"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\u2013163. ACM, New York, NY, USA (2010). http:\/\/doi.acm.org\/10.1145\/1850771.1850793","DOI":"10.1145\/1850771.1850793"},{"issue":"4","key":"15_CR7","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1007\/s100090050043","volume":"2","author":"K Havelund","year":"2000","unstructured":"Havelund, K., Pressburger, T.: Model checking JAVA programs using JAVA PathFinder. Int. J. Softw. Tools Technol. Transf. 2(4), 366\u2013381 (2000). http:\/\/dx.doi.org\/10.1007\/s100090050043","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"15_CR8","unstructured":"Hoare, C.A.R.: Communicating sequential processes (2004). www.usingcsp.com\/cspbook.pdf"},{"key":"15_CR9","unstructured":"IceLab. www.icelab.dk\/index.html"},{"key":"15_CR10","doi-asserted-by":"crossref","unstructured":"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\u2013174. ACM, New York, NY, USA (2010). http:\/\/doi.acm.org\/10.1145\/1850771.1850794","DOI":"10.1145\/1850771.1850794"},{"key":"15_CR11","unstructured":"Luckcuck, M.: hiJaC Case Studies (2016). www.cs.york.ac.uk\/circus\/hijac\/case.html . Accessed 14 Jan 2016"},{"key":"15_CR12","unstructured":"Luckcuck, M.: Safety-Critical Java Level 2 Framework Model (2016). www.cs.york.ac.uk\/circus\/publications\/techreports\/reports\/SCJLevel2Framework.pdf"},{"key":"15_CR13","unstructured":"Luckcuck, M., Wellings, A., Cavalcanti, A.: Safety-Critical Java: Level 2 in Practice (submitted)"},{"key":"15_CR14","volume-title":"Programming from Specifications","author":"C Morgan","year":"1990","unstructured":"Morgan, C.: Programming from Specifications. Prentice-Hall, Inc., USA (1990)"},{"issue":"1\u20132","key":"15_CR15","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1016\/j.sysarc.2007.06.001","volume":"54","author":"M Schoeberl","year":"2008","unstructured":"Schoeberl, M.: A Java processor architecture for embedded real-time systems. J. Syst. Architect. 54(1\u20132), 265\u2013286 (2008). www.sciencedirect.com\/science\/article\/pii\/S1383762107000963","journal-title":"J. Syst. Architect."},{"issue":"2","key":"15_CR16","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1007\/s00165-009-0119-6","volume":"22","author":"A Sherif","year":"2009","unstructured":"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\u2013191 (2009)","journal-title":"Formal Aspects Comput."},{"key":"15_CR17","doi-asserted-by":"crossref","unstructured":"S\u00f8ndergaard, 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\u201353. ACM, New York, NY, USA (2012)","DOI":"10.1145\/2388936.2388945"},{"key":"15_CR18","unstructured":"Spivey, J.M.: The Z Notation: A Reference Manual. International Series in Computer Science. Prentice-Hall, Inc. Upper Saddle River (1992)"},{"key":"15_CR19","doi-asserted-by":"crossref","unstructured":"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\u2013154. ACM, Prague, Czech Republic (2010)","DOI":"10.1145\/1850771.1850792"},{"key":"15_CR20","unstructured":"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"},{"key":"15_CR21","unstructured":"The Real-Time for Java Expert Group: Real-Time Specification for Java Language Specification (2005). www.timesys.com\/java\/"},{"key":"15_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1007\/978-3-319-25527-9_21","volume-title":"Programming Languages with Applications to Biology and Security","author":"B Thomsen","year":"2015","unstructured":"Thomsen, B., Luckow, K.S., Leth, L., B\u00f8gholm, T.: From safety critical java programs to timed process models. In: Burrows, M., et al. (eds.) Degano Festschrift. LNCS, vol. 9465, pp. 319\u2013338. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-25527-9_21"},{"key":"15_CR23","doi-asserted-by":"crossref","unstructured":"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\u201357. ACM, New York, NY, USA (2013). http:\/\/doi.acm.org\/10.1145\/2512989.2512991","DOI":"10.1145\/2512989.2512991"},{"key":"15_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"184","DOI":"10.1007\/3-540-45648-1_10","volume-title":"ZB 2002: Formal Specification and Development in Z and B","author":"J Woodcock","year":"2002","unstructured":"Woodcock, J., Cavalcanti, A.: The semantics of $$Circus$$ C i r c u s . In: Bert, D., Bowen, J.P., C. Henson, M., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, pp. 184\u2013203. Springer, Heidelberg (2002)"},{"key":"15_CR25","doi-asserted-by":"crossref","first-page":"1046","DOI":"10.1093\/comjnl\/bxt060","volume":"57","author":"F Zeyda","year":"2013","unstructured":"Zeyda, F., Lalkhumsanga, L., Cavalcanti, A., Wellings, A.: Circus models for safety-critical Java programs. Comput. J. 57, 1046\u20131091 (2013). http:\/\/comjnl.oxfordjournals.org\/content\/early\/2013\/07\/02\/comjnl.bxt060.abstract","journal-title":"Comput. J."}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-33693-0_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T10:43:52Z","timestamp":1498301032000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-33693-0_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319336923","9783319336930"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-33693-0_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}