{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T06:37:10Z","timestamp":1759991830149},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319294728"},{"type":"electronic","value":"9783319294735"}],"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-29473-5_6","type":"book-chapter","created":{"date-parts":[[2016,1,23]],"date-time":"2016-01-23T07:58:11Z","timestamp":1453535891000},"page":"93-109","source":"Crossref","is-referenced-by-count":1,"title":["Refinement Strategies for Safety-Critical Java"],"prefix":"10.1007","author":[{"given":"Alvaro","family":"Miyazawa","sequence":"first","affiliation":[]},{"given":"Ana","family":"Cavalcanti","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,1,24]]},"reference":[{"key":"6_CR1","unstructured":"Miyazawa, A., Cavalcanti, A.: Report on refinement strategies for Safety-Critical Java (2015). \n                      http:\/\/www-users.cs.york.ac.uk\/~alvarohm\/report2015b.pdf"},{"issue":"3","key":"6_CR2","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/s10009-004-0167-4","volume":"7","author":"L Burdy","year":"2005","unstructured":"Burdy, L., et al.: An overview of JML tools and applications. Int. J. Softw. Tools Technol. Transf. 7(3), 212\u2013232 (2005)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"3","key":"6_CR3","doi-asserted-by":"publisher","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)","journal-title":"Softw. Syst. Model."},{"issue":"4","key":"6_CR4","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. Formal Aspects Comput. 23(4), 465\u2013512 (2011)","journal-title":"Formal Aspects Comput."},{"issue":"5","key":"6_CR5","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., et al.: Safety-Critical Java programs from Circus models. Real-Time Syst. 49(5), 614\u2013667 (2013)","journal-title":"Real-Time Syst."},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"Haddad, G., et al.: The design of SafeJML, a specification language for SCJ with supportfor WCET specification. In: JTRES 2010, pp. 155\u2013163. ACM (2010)","DOI":"10.1145\/1850771.1850793"},{"key":"6_CR7","unstructured":"Locke, D., et al.: Safety-Critical Java technology specification. Technical report"},{"key":"6_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"336","DOI":"10.1007\/978-3-642-38164-5_23","volume-title":"Computation, Logic, Games, and Quantum Foundations","author":"J Benthem van","year":"2013","unstructured":"van Benthem, J.: Reasoning about strategies. In: Coecke, B., Ong, L., Panangaden, P. (eds.) Computation, Logic, Games and Quantum Foundations. LNCS, vol. 7860, pp. 336\u2013347. Springer, Heidelberg (2013)"},{"key":"6_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1007\/978-3-319-10181-1_10","volume-title":"Integrated Formal Methods","author":"A Miyazawa","year":"2014","unstructured":"Miyazawa, A., Cavalcanti, A.: Formal refinement in SysML. In: Albert, E., Sekerinski, E. (eds.) IFM 2014. LNCS, vol. 8739, pp. 155\u2013170. Springer, Heidelberg (2014)"},{"key":"6_CR10","unstructured":"Miyazawa, A., Cavalcanti, A.: Refinement of Circus models into SCJ-Circus (2015). \n                      http:\/\/www-users.cs.york.ac.uk\/~alvarohm\/report2015a.pdf"},{"issue":"10\u201311","key":"6_CR11","doi-asserted-by":"publisher","first-page":"1151","DOI":"10.1016\/j.scico.2011.07.007","volume":"77","author":"A Miyazawa","year":"2012","unstructured":"Miyazawa, A., Cavalcanti, A.L.C.: Refinement-oriented models of Stateflow charts. Sci. Comput. Program. 77(10\u201311), 1151\u20131177 (2012)","journal-title":"Sci. Comput. Program."},{"key":"6_CR12","doi-asserted-by":"crossref","unstructured":"Miyazawa, A., Cavalcanti, A.L.C.: SCJ-Circus: a refinement-oriented formal notation for Safety-Critical Java. In: Refinement Workshop (2015)","DOI":"10.4204\/EPTCS.209.6"},{"key":"6_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-3-642-41202-8_17","volume-title":"Formal Methods and Software Engineering","author":"A Miyazawa","year":"2013","unstructured":"Miyazawa, A., Lima, L., Cavalcanti, A.: Formal models of SysML blocks. In: Groves, L., Sun, J. (eds.) ICFEM 2013. LNCS, vol. 8144, pp. 249\u2013264. Springer, Heidelberg (2013)"},{"key":"6_CR14","unstructured":"Oliveira, M.V.M.: Formal derivation of state-rich reactive programs using Circus. Ph.D. thesis, University of York (2006)"},{"key":"6_CR15","volume-title":"Understanding Concurrent Systems: Texts in Computer Science","author":"AW Roscoe","year":"2011","unstructured":"Roscoe, A.W.: Understanding Concurrent Systems: Texts in Computer Science. Springer, London (2011)"},{"key":"6_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/978-3-642-35705-3_3","volume-title":"Unifying Theories of Programming","author":"K Wei","year":"2012","unstructured":"Wei, K., Woodcock, J.C.P., Cavalcanti, A.L.C.: Circus Time with Reactive Designs. In: Wolff, B., Gaudel, M.-C., Feliachi, A. (eds.) UTP 2012. LNCS, vol. 7681, pp. 68\u201387. Springer, Heidelberg (2012)"},{"key":"6_CR17","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":"6_CR18","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, New York (1996)"},{"key":"6_CR19","unstructured":"Zeyda, F., Cavalcanti, A., Wellings, A., Woodcock, J., Wei, K.: Refinement of the Parallel CDx. Technical report, University of York (2012)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods: Foundations and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-29473-5_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T11:14:56Z","timestamp":1559387696000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-29473-5_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319294728","9783319294735"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-29473-5_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}