{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T04:37:09Z","timestamp":1725856629650},"publisher-location":"Cham","reference-count":36,"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_5","type":"book-chapter","created":{"date-parts":[[2016,5,24]],"date-time":"2016-05-24T01:35:47Z","timestamp":1464053747000},"page":"63-78","source":"Crossref","is-referenced-by-count":2,"title":["Modelling and Verifying a Priority Scheduler for an SCJ Runtime Environment"],"prefix":"10.1007","author":[{"given":"Leo","family":"Freitas","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"James","family":"Baxter","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ana","family":"Cavalcanti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andy","family":"Wellings","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,5,24]]},"reference":[{"issue":"1","key":"5_CR1","first-page":"5:1","volume":"7","author":"A Armbruster","year":"2007","unstructured":"Armbruster, A., et al.: A real-time Java virtual machine with applications in avionics. ACM TECS 7(1), 5:1\u20135:49 (2007)","journal-title":"ACM TECS"},{"key":"5_CR2","unstructured":"Atego: Atego PERC Pico - Products - Atego (2015). www.atego.com\/products\/atego-perc-pico\/"},{"issue":"5","key":"5_CR3","doi-asserted-by":"crossref","first-page":"284","DOI":"10.1049\/sej.1993.0034","volume":"8","author":"N Audsley","year":"1993","unstructured":"Audsley, N., Burns, A., Richardson, M., Tindell, K., Wellings, A.J.: Applying new scheduling theory to static priority pre-emptive scheduling. Softw. Eng. J. 8(5), 284\u2013292 (1993)","journal-title":"Softw. Eng. J."},{"key":"5_CR4","unstructured":"Baxter, J.: Requirements for Safety-Critical Java Virtual Machines. Technical report, University of York (2015). http:\/\/www.cs.york.ac.uk\/circus\/publications\/techreports\/reports\/scjvm-requirements.pdf"},{"issue":"3","key":"5_CR5","first-page":"277","volume":"4","author":"ALC Cavalcanti","year":"2005","unstructured":"Cavalcanti, A.L.C., Sampaio, A.C.A., Woodcock, J.C.P.: Unifying classes and processes. SoSyM 4(3), 277\u2013296 (2005)","journal-title":"SoSyM"},{"issue":"5","key":"5_CR6","first-page":"614","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 $${\\sf Circus}$$ Circus models. RTS 49(5), 614\u2013667 (2013)","journal-title":"RTS"},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"Dalsgaard, A.E., Hansen, R.R., Schoeberl, M.: Private memory allocation analysis for safety-critical Java. In: JTRES, pp. 9\u201317. ACM (2012)","DOI":"10.1145\/2388936.2388939"},{"issue":"4","key":"5_CR8","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1007\/s10009-014-0307-4","volume":"16","author":"J Ferreira","year":"2014","unstructured":"Ferreira, J., et al.: Automated verification of the FreeRTOS scheduler in Hip\/Sleek. STTT 16(4), 381\u2013397 (2014)","journal-title":"STTT"},{"issue":"5","key":"5_CR9","doi-asserted-by":"crossref","first-page":"463","DOI":"10.1007\/s10009-011-0195-9","volume":"13","author":"L Freitas","year":"2011","unstructured":"Freitas, L., McDermott, J.P.: Formal methods for security in the Xenon hypervisor. STTT 13(5), 463\u2013489 (2011)","journal-title":"STTT"},{"issue":"1","key":"5_CR10","first-page":"117","volume":"20","author":"L Freitas","year":"2008","unstructured":"Freitas, L., Woodcock, J.C.P.: Mechanising mondex with Z\/Eves. FACJ 20(1), 117\u2013139 (2008)","journal-title":"FACJ"},{"issue":"4","key":"5_CR11","first-page":"238","volume":"74","author":"L Freitas","year":"2009","unstructured":"Freitas, L., Woodcock, J.C.P., Fu, Z.: POSIX file store in Z\/Eves: an experiment in the verified software repository. SCP 74(4), 238\u2013257 (2009)","journal-title":"SCP"},{"key":"5_CR12","unstructured":"Freitas, L., Cavalcanti, A., Wellings, A.: Formal specification of SCJ icecap-implementation. Technical report, Newcastle University (2015). https:\/\/www.cs.york.ac.uk\/circus\/publications\/techreports\/reports\/hvm.pdf"},{"key":"5_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1007\/978-3-540-79707-4_8","volume-title":"Formal Methods for Industrial Critical Systems","author":"L Gesellensetter","year":"2008","unstructured":"Gesellensetter, L., Glesner, S., Salecker, E.: Formal verification with Isabelle\/HOL in practice: finding a bug in the GCC scheduler. In: Leue, S., Merino, P. (eds.) FMICS 2007. LNCS, vol. 4916, pp. 85\u2013100. Springer, Heidelberg (2008)"},{"key":"5_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1007\/978-3-642-54862-8_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Gibson-Robinson","year":"2014","unstructured":"Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3 \u2014 a modern refinement checker for CSP. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 187\u2013201. Springer, Heidelberg (2014)"},{"key":"5_CR15","first-page":"452","volume":"23","author":"A Gotsman","year":"2013","unstructured":"Gotsman, A., Yang, H.: Modular verification of preemptive OS kernels. JFP 23, 452\u2013514 (2013)","journal-title":"JFP"},{"key":"5_CR16","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: JTRES. ACM (2010)","DOI":"10.1145\/1850771.1850793"},{"key":"5_CR17","volume-title":"Communicating Sequential Processes","author":"CAR Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Upper Saddle River (1985)"},{"key":"5_CR18","unstructured":"aicas realtime.: JamaicaVM User Manual (2014). www.aicas.com\/cms\/en\/reference-material"},{"issue":"1","key":"5_CR19","first-page":"2:1","volume":"32","author":"G Klein","year":"2014","unstructured":"Klein, G., et al.: Comprehensive formal verification of an OS microkernel. ACM TCS 32(1), 2:1\u20132:70 (2014)","journal-title":"ACM TCS"},{"key":"5_CR20","volume-title":"Safety Critical Java Specification","author":"D Locke","year":"2010","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. The Open Group, UK (2010)"},{"key":"5_CR21","doi-asserted-by":"crossref","unstructured":"Luckowe, K.S., Thomsen, B., Korsholm, S.E.: HVMTP: a time predictable and portable java virtual machine for hard real-time embedded systems. In: JTRES, pp. 107\u2013 116. ACM (2014)","DOI":"10.1145\/2661020.2661022"},{"key":"5_CR22","doi-asserted-by":"crossref","unstructured":"Ludwich, M.K., Frohlich, A.A.: System-level verification of embedded operating systems components. In: SBESC, pp. 161\u2013165, November 2012","DOI":"10.1109\/SBESC.2012.39"},{"key":"5_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1007\/11415787_5","volume-title":"ZB 2005: Formal Specification and Development in Z and B","author":"P Malik","year":"2005","unstructured":"Malik, P., Utting, M.: CZT: a framework for Z tools. In: Treharne, H., King, S., C. Henson, M., Schneider, S. (eds.) ZB 2005. LNCS, vol. 3455, pp. 65\u201384. Springer, Heidelberg (2005)"},{"key":"5_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1007\/978-3-319-06410-9_32","volume-title":"FM 2014: Formal Methods","author":"C Marriott","year":"2014","unstructured":"Marriott, C., Cavalcanti, A.: SCJ: memory-safety checking without annotations. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 465\u2013480. Springer, Heidelberg (2014)"},{"key":"5_CR25","unstructured":"Meisels, I.: Software Manual for Windows Z\/EVES Version 2.1. ORA Canada, tR-97-5505-04g (2000)"},{"issue":"1\u20132","key":"5_CR26","first-page":"3","volume":"21","author":"MVM Oliveira","year":"2009","unstructured":"Oliveira, M.V.M., Cavalcanti, A.L.C., Woodcock, J.C.P.: A UTP semantics for $${\\sf Circus}$$ Circus . FACJ 21(1\u20132), 3\u201332 (2009)","journal-title":"FACJ"},{"key":"5_CR27","unstructured":"Oliveira, M., Sampaio, A.: Compositional analysis and design of CML models. Technical report D24.1, COMPASS, March 2013. www.compass-research.eu\/Project\/Deliverables\/D241.pdf"},{"key":"5_CR28","doi-asserted-by":"crossref","unstructured":"Pizlo, F., Ziarek, L., Vitek, J.: Real time Java on resource-constrained platforms with Fiji VM. In: JTRES, pp. 110\u2013119. ACM (2009)","DOI":"10.1145\/1620405.1620421"},{"key":"5_CR29","unstructured":"Richard-Foy, M., et al.: Use of PERC Pico for safety critical Java. In: ERTS (2010)"},{"key":"5_CR30","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":"5_CR31","unstructured":"Saaltink, M.: Z\/Eves 2.0 user\u2019s guide. Technical report. TR-99-5493-06a, ORA Canada (1999)"},{"key":"5_CR32","doi-asserted-by":"crossref","unstructured":"S\u00f8ndergaard, H., Korsholm, S.E., Ravn, A.P.: Safety-critical Java for low-end embedded platforms. In: JTRES, pp. 44\u201353. ACM (2012)","DOI":"10.1145\/2388936.2388945"},{"key":"5_CR33","doi-asserted-by":"crossref","unstructured":"Tang, D., Plsek, A., Vitek, J.: Static Checking of Safety Critical Java Annotations. In: JTRES. ACM (2010)","DOI":"10.1145\/1850771.1850792"},{"issue":"2","key":"5_CR34","doi-asserted-by":"crossref","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":"5_CR35","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":"5_CR36","unstructured":"Woodcock, J.C.P., Davies, J.: Using Z-specification, refinement, and proof. Prentice-Hall, Upper Saddle River (1996)"}],"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_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T10:43:50Z","timestamp":1498301030000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-33693-0_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319336923","9783319336930"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-33693-0_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}