{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T04:38:05Z","timestamp":1743136685829,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662468227"},{"type":"electronic","value":"9783662468234"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46823-4_14","type":"book-chapter","created":{"date-parts":[[2015,4,18]],"date-time":"2015-04-18T01:40:54Z","timestamp":1429321254000},"page":"161-176","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["A Proof-Based Method for Modelling Timed Systems"],"prefix":"10.1007","author":[{"given":"Alexei","family":"Iliasov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jeremy","family":"Bryans","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,4,19]]},"reference":[{"key":"14_CR1","unstructured":"Iliasov, A., Bryans, J.: Event-B development of Fischer\u2019s algorithm. http:\/\/iliasov.org\/fischer"},{"key":"14_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BFb0031985","volume-title":"Real-Time: Theory in Practice","author":"M Abadi","year":"1992","unstructured":"Abadi, M., Lamport, L.: An old-fashioned recipe for real time. In: Huizing, C., de Bakker, J.W., Rozenberg, G., de Roever, W.-P. (eds.) REX 1991. LNCS, vol. 600, pp. 1\u201327. Springer, Heidelberg (1992)"},{"key":"14_CR3","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, New York (2005)"},{"key":"14_CR4","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. Cambridge University Press, New York (2010)"},{"key":"14_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/BFb0032042","volume-title":"Automata, Languages and Programming","author":"R Alur","year":"1990","unstructured":"Alur, R., Dill, D.L.: Automata for modeling real-time systems. In: Paterson, M. (ed.) ICALP 1990. LNCS, vol. 443, pp. 322\u2013335. Springer, Heidelberg (1990)"},{"key":"14_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/3-540-48119-2_22","volume-title":"FM\u201999 - Formal Methods","author":"P Behm","year":"1999","unstructured":"Behm, P., Benoit, P., Faivre, A., Meynadier, J.-M.: M\u00e9t\u00e9or: a successful application of B in a large project. In: Wing, J.M., Woodcock, J. (eds.) FM 1999. LNCS, vol. 1708, p. 369. Springer, Heidelberg (1999)"},{"key":"14_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/BFb0020949","volume-title":"Hybrid Systems III","author":"J Bengtsson","year":"1996","unstructured":"Bengtsson, J., Larsen, K., Larsson, F., Pettersson, P., Yi, W.: Uppaal - a tool suite for automatic verification of real-time systems. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) HS 1995. LNCS, vol. 1066, pp. 232\u2013243. Springer, Heidelberg (1996)"},{"key":"14_CR8","unstructured":"Butler, M., Falampin, J.: An approach to modelling and refining timing properties in B. In: Refinement of Critical Systems (RCS), January 2002"},{"key":"14_CR9","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)"},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"Davies, J.: Specification and Proof in Real-time CSP (1993)","DOI":"10.1017\/CBO9780511569760"},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"Futch, M.J.: Leibniz\u2019s Metaphysics of Time and Space (2008)","DOI":"10.1007\/978-1-4020-8237-5"},{"key":"14_CR12","unstructured":"Jensen, H.E.: Abstraction-based verification of distributed systems. Technical report, Aalborg University, Department of Computer Science (1999)"},{"key":"14_CR13","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-1494-9","volume-title":"The B Language and Method: A Guide to Practical Formal Development","author":"K Lano","year":"1996","unstructured":"Lano, K.: The B Language and Method: A Guide to Practical Formal Development. Springer-Verlag New York, Inc., Secaucus (1996)"},{"key":"14_CR14","unstructured":"Luchangco, V.: Using Simulation Techniques to Prove Timing Properties (1995)"},{"key":"14_CR15","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1996.0060","volume":"128","author":"N Lynch","year":"1996","unstructured":"Lynch, N., Vaandrager, F.: Forward and backward simulations - part II: Timing-based systems. Inf. Comput. 128, 1\u201325 (1996)","journal-title":"Inf. Comput."},{"key":"14_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"401","DOI":"10.1007\/BFb0039073","volume-title":"CONCUR \u201990","author":"F Moller","year":"1990","unstructured":"Moller, F., Tofts, C.: A temporal calculus of communicating systems. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 401\u2013415. Springer, Heidelberg (1990)"},{"key":"14_CR17","unstructured":"RODIN. Event-B Platform (2009). http:\/\/www.event-b.org\/"},{"key":"14_CR18","unstructured":"de Roever, W.-P., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and Their Comparison (2008)"},{"key":"14_CR19","volume-title":"Concurrent and Real Time Systems: The CSP Approach","author":"S Schneider","year":"1999","unstructured":"Schneider, S.: Concurrent and Real Time Systems: The CSP Approach. Wiley, New York (1999)"}],"container-title":["Lecture Notes in Computer Science","Perspectives of System Informatics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46823-4_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,20]],"date-time":"2023-01-20T07:01:34Z","timestamp":1674198094000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-46823-4_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662468227","9783662468234"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46823-4_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"19 April 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}