{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T10:28:45Z","timestamp":1777544925822,"version":"3.51.4"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319246437","type":"print"},{"value":"9783319246444","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","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":[[2015]]},"DOI":"10.1007\/978-3-319-24644-4_20","type":"book-chapter","created":{"date-parts":[[2015,9,24]],"date-time":"2015-09-24T01:34:39Z","timestamp":1443058479000},"page":"292-307","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["An Interval-Based Approach to Modelling Time in Event-B"],"prefix":"10.1007","author":[{"given":"Gintautas","family":"Sulskus","sequence":"first","affiliation":[]},{"given":"Michael","family":"Poppleton","sequence":"additional","affiliation":[]},{"given":"Abdolbaghi","family":"Rezazadeh","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,11,12]]},"reference":[{"key":"20_CR1","unstructured":"Pacemaker Challenge (2007). \n                    \n                      http:\/\/sqrl.mcmaster.ca\/pacemaker.htm"},{"key":"20_CR2","unstructured":"Interactive Prover Reference Manual 3.7 (2013). \n                    \n                      http:\/\/www.atelierb.eu\/ressources\/DOC\/english\/prover-reference-manual.pdf"},{"key":"20_CR3","unstructured":"iUML (2013). \n                    \n                      http:\/\/wiki.event-b.org\/index.php\/IUML-B"},{"key":"20_CR4","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, New York (1996)","DOI":"10.1017\/CBO9780511624162"},{"key":"20_CR5","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"J.-R. Abrial","year":"2010","unstructured":"Abrial, J.-R.: Modeling in Event-B: System and Software Engineering, 1st edn. Cambridge University Press, New York (2010)","edition":"1"},{"issue":"6","key":"20_CR6","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/s10009-010-0145-y","volume":"12","author":"J.-R. Abrial","year":"2010","unstructured":"Abrial, J.-R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an Open Toolset for Modelling and Reasoning in Event-B. International Journal on Software Tools for Technology Transfer\u00a012(6), 447\u2013466 (2010)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"20_CR7","doi-asserted-by":"crossref","unstructured":"Back, R.-J., Kurki-Suonio, R.: Decentralization of Process Nets with Centralized Control. In: Symposium on Principles of Distributed Computing, pp. 131\u2013142. ACM, Montreal (1983)","DOI":"10.1145\/800221.806716"},{"key":"20_CR8","doi-asserted-by":"crossref","unstructured":"Barold, S.S., Stroobandt, R., Sinnaeve, A.F.: Cardiac Pacemakers and Resynchronization Step-by-Step: an Illustrated Guide. Wiley-Blackwell (2010)","DOI":"10.1002\/9781444323214"},{"key":"20_CR9","unstructured":"Bendisposto, J.: ProB 2.0 Developer Handbook (2014). \n                    \n                      http:\/\/nightly.cobra.cs.uni-duesseldorf.de\/prob2\/developer-documentation\/prob-devel.pdf"},{"key":"20_CR10","first-page":"105","volume-title":"Patterns for Modelling Time and Consistency in Business Information Systems","author":"J. Bryans","year":"2010","unstructured":"Bryans, J., Fitzgerald, J., Romanovsky, A., Roth, A.: Patterns for Modelling Time and Consistency in Business Information Systems, pp. 105\u2013114. IEEE Computer Society, Oxford (2010)"},{"key":"20_CR11","unstructured":"Butler, M., Falampin, J.: An Approach to Modelling and Refining Timing Properties in B. In: Proceedings of Workshop on Refinement of Critical Systems (RCS) (January 2002)"},{"key":"20_CR12","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.\u00a04355, pp. 140\u2013154. Springer, Heidelberg (2006)"},{"key":"20_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/978-3-642-30885-7_14","volume-title":"Abstract State Machines, Alloy, B, VDM, and Z","author":"D. D\u00e9harbe","year":"2012","unstructured":"D\u00e9harbe, D., Fontaine, P., Guyot, Y., Voisin, L.: SMT Solvers for Rodin. In: Derrick, J., Fitzgerald, J., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.) ABZ 2012. LNCS, vol.\u00a07316, pp. 194\u2013207. Springer, Heidelberg (2012)"},{"key":"20_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1007\/978-3-642-19829-8_14","volume-title":"Formal Methods: Foundations and Applications","author":"A.O. Gomes","year":"2011","unstructured":"Gomes, A.O., Oliveira, M.: Formal Development of a Cardiac Pacemaker: From Specification to Code. In: Davies, J. (ed.) SBMF 2010. LNCS, vol.\u00a06527, pp. 210\u2013225. Springer, Heidelberg (2011)"},{"key":"20_CR15","doi-asserted-by":"crossref","unstructured":"Jee, E., Wang, S., Kim, J.K., Lee, J., Sokolsky, O., Lee, I.: A Safety-Assured Development Approach for Real-Time Software. In: The Proceedings of the 16th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications, pp. 133\u2013142 (August 2010)","DOI":"10.1109\/RTCSA.2010.42"},{"key":"20_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-642-28756-5_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Z. Jiang","year":"2012","unstructured":"Jiang, Z., Pajic, M., Moarref, S., Alur, R., Mangharam, R.: Modeling and Verification of a Dual Chamber Implantable Pacemaker. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol.\u00a07214, pp. 188\u2013203. Springer, Heidelberg (2012)"},{"key":"20_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"855","DOI":"10.1007\/978-3-540-45236-2_46","volume-title":"FME 2003: Formal Methods","author":"M. Leuschel","year":"2003","unstructured":"Leuschel, M., Butler, M.: ProB: A Model Checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805, pp. 855\u2013874. Springer, Heidelberg (2003)"},{"key":"20_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/978-3-540-68237-0_14","volume-title":"FM 2008: Formal Methods","author":"H. Macedo","year":"2008","unstructured":"Macedo, H., Larsen, P., Fitzgerald, J.: Incremental Development of a Distributed Real-Time Model of a Cardiac Pacing System Using VDM. In: Cuellar, J., Sere, K. (eds.) FM 2008. LNCS, vol.\u00a05014, pp. 181\u2013197. Springer, Heidelberg (2008)"},{"key":"20_CR19","unstructured":"M\u00e9ry, D., Singh, N.K.: Pacemaker\u2019s Functional Behaviors in Event-B. Research Report inria-00419973 (2009)"},{"key":"20_CR20","unstructured":"Rehm, J.: From Absolute-Timer to Relative-Countdown: Patterns for Model-Checking (May 2008) (Unpublished)"},{"key":"20_CR21","unstructured":"Sarshogh, M.R.: Extending Event-B with Discrete Timing Properties. PhD thesis, University of Southampton (2013)"},{"key":"20_CR22","unstructured":"Savicks, V., Butler, M., Colley, J.: Co-simulating Event-B and Continuous Models via FMI. In: 2014 Summer Computer Simulation Conference, Society for Modeling & Simulation International (SCS) (July 2014)"},{"key":"20_CR23","unstructured":"Sulskus, G., Poppleton, M., Rezazadeh, A.: Example Event-B project (2014). \n                    \n                      http:\/\/users.ecs.soton.ac.uk\/gs6g10\/SimplifiedPMExample.zip"},{"key":"20_CR24","unstructured":"Sulskus, G., Poppleton, M., Rezazadeh, A.: An Investigation into Event-B Methodologies and Timing Constraint Modelling. Mini-Thesis, University of Southampton (2014)"},{"key":"20_CR25","unstructured":"Wang, J.: Handbook of Finite State Based Models and Applications. Discrete Mathematics and Its Applications. Chapman and Hall\/CRC (2012)"},{"key":"20_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"438","DOI":"10.1007\/978-3-642-20398-5_31","volume-title":"NASA Formal Methods","author":"F. Yang","year":"2011","unstructured":"Yang, F., Jacquot, J.-P.: Scaling Up with Event-B: A Case Study. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol.\u00a06617, pp. 438\u2013452. Springer, Heidelberg (2011)"}],"container-title":["Lecture Notes in Computer Science","Fundamentals of Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-24644-4_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,23]],"date-time":"2019-09-23T20:03:39Z","timestamp":1569269019000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-24644-4_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319246437","9783319246444"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24644-4_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"12 November 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}