{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,5]],"date-time":"2025-04-05T21:05:17Z","timestamp":1743887117208},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319912707"},{"type":"electronic","value":"9783319912714"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"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":[[2018]]},"DOI":"10.1007\/978-3-319-91271-4_15","type":"book-chapter","created":{"date-parts":[[2018,5,7]],"date-time":"2018-05-07T10:32:55Z","timestamp":1525689175000},"page":"219-233","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Refinement of Timing Constraints for Concurrent Tasks with Scheduling"],"prefix":"10.1007","author":[{"given":"Chenyang","family":"Zhu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Butler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Corina","family":"Cirstea","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,5,8]]},"reference":[{"key":"15_CR1","volume-title":"The B-Book: Assigning Programs to Meanings","author":"JR Abrial","year":"2005","unstructured":"Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (2005)"},{"key":"15_CR2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"JR Abrial","year":"2010","unstructured":"Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)"},{"doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.A.: Finitary fairness. In: Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science, pp. 52\u201361, July 1994","key":"15_CR3","DOI":"10.1109\/LICS.1994.316087"},{"key":"15_CR4","volume-title":"Principles of Cyber-Physical Systems","author":"R Alur","year":"2015","unstructured":"Alur, R.: Principles of Cyber-Physical Systems. The MIT Press, Cambridge (2015)"},{"issue":"2","key":"15_CR5","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theoret. Comput. Sci. 126(2), 183\u2013235 (1994)","journal-title":"Theoret. Comput. Sci."},{"key":"15_CR6","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1016\/j.scico.2015.02.003","volume":"105","author":"R Banach","year":"2015","unstructured":"Banach, R., Butler, M., Qin, S., Verma, N., Zhu, H.: Core hybrid Event-B I: single hybrid Event-B machines. Sci. Comput. Program. 105, 92\u2013123 (2015)","journal-title":"Sci. Comput. Program."},{"key":"15_CR7","volume-title":"Mastering System Analysis and Design through Abstraction and Refinement","author":"M Butler","year":"2013","unstructured":"Butler, M.: Mastering System Analysis and Design through Abstraction and Refinement. IOS Press, Amsterdam (2013). \nhttp:\/\/eprints.soton.ac.uk\/349769\/"},{"key":"15_CR8","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1201\/b20053-5","volume-title":"From Action Systems to Distributed Systems","author":"Michael Butler","year":"2016","unstructured":"Butler, M., Abrial, J.R., Banach, R.: Modelling and refining hybrid systems in Event-B and Rodin. In: Petre, L., Sekerinski, E. (eds.) From Action System to Distributed Systems: The Refinement Approach. Taylor & Francis, April 2016. \nhttps:\/\/eprints.soton.ac.uk\/376053\/"},{"unstructured":"Butler, M., Falampin, J.: An approach to modelling and refining timing properties in B, January 2002. \nhttps:\/\/eprints.soton.ac.uk\/256235\/","key":"15_CR9"},{"key":"15_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/11955757_13","volume-title":"B 2007: Formal Specification and Development in B","author":"D Cansell","year":"2006","unstructured":"Cansell, D., M\u00e9ry, D., Rehm, J.: Time constraint patterns for Event B development. In: Julliand, J., Kouchnarenko, O. (eds.) B 2007. LNCS, vol. 4355, pp. 140\u2013154. Springer, Heidelberg (2006). \nhttps:\/\/doi.org\/10.1007\/11955757_13"},{"key":"15_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/978-3-540-39910-0_14","volume-title":"Verification: Theory and Practice","author":"N Dershowitz","year":"2003","unstructured":"Dershowitz, N., Jayasimha, D.N., Park, S.: Bounded fairness. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol. 2772, pp. 304\u2013317. Springer, Heidelberg (2003). \nhttps:\/\/doi.org\/10.1007\/978-3-540-39910-0_14"},{"key":"15_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-540-75454-1_10","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"H Dierks","year":"2007","unstructured":"Dierks, H., Kupferschmid, S., Larsen, K.G.: Automatic abstraction refinement for timed automata. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 114\u2013129. Springer, Heidelberg (2007). \nhttps:\/\/doi.org\/10.1007\/978-3-540-75454-1_10"},{"key":"15_CR13","first-page":"143","volume":"77","author":"S Graf","year":"2007","unstructured":"Graf, S., Prinz, A.: Time in state machines. Fundam. Inform. 77, 143\u2013174 (2007)","journal-title":"Fundam. Inform."},{"key":"15_CR14","series-title":"2.8covers Rodin","volume-title":"Rodin User\u2019s Handbook: Covers Rodin V.2.8","author":"M Jastram","year":"2014","unstructured":"Jastram, M., Butler, P.: Rodin User\u2019s Handbook: Covers Rodin V.2.8. 2.8covers Rodin. Createspace Independent Pub, North Charleston (2014). \nhttps:\/\/books.google.co.uk\/books?id=ws2WoAEACAAJ"},{"issue":"1\u20132","key":"15_CR15","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"KG Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Int. J. Softw. Tools Technol. Transf. 1(1\u20132), 134\u2013152 (1997)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"unstructured":"Sarshogh, M.R., Butler, M.: Specification and refinement of discrete timing properties in Event-B. In: AVoCS 2011 (2011). \nhttps:\/\/eprints.soton.ac.uk\/272480\/","key":"15_CR16"},{"unstructured":"Sekerinski, E., Zhang, T.: Finitary fairness in Event-B. In: Dagstuhl Seminar on Refinement Based Methods for the Construction of Dependable Systems. Dagstuhl, Germany (2009)","key":"15_CR17"},{"key":"15_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/978-3-642-39718-9_19","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2013","author":"E Sekerinski","year":"2013","unstructured":"Sekerinski, E., Zhang, T.: Finitary fairness in action systems. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) ICTAC 2013. LNCS, vol. 8049, pp. 319\u2013336. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-39718-9_19"},{"key":"15_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/978-3-319-24644-4_20","volume-title":"Fundamentals of Software Engineering","author":"G Sulskus","year":"2015","unstructured":"Sulskus, G., Poppleton, M., Rezazadeh, A.: An interval-based approach to modelling time in Event-B. In: Dastani, M., Sirjani, M. (eds.) FSEN 2015. LNCS, vol. 9392, pp. 292\u2013307. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-24644-4_20\n\n. \nhttp:\/\/eprints.soton.ac.uk\/377201\/"}],"container-title":["Lecture Notes in Computer Science","Abstract State Machines, Alloy, B, TLA, VDM, and Z"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-91271-4_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,5,7]],"date-time":"2018-05-07T10:40:22Z","timestamp":1525689622000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-91271-4_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319912707","9783319912714"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-91271-4_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}