{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T04:05:31Z","timestamp":1748664331892,"version":"3.41.0"},"publisher-location":"Cham","reference-count":11,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319231280"},{"type":"electronic","value":"9783319231297"}],"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-319-23129-7_3","type":"book-chapter","created":{"date-parts":[[2015,8,27]],"date-time":"2015-08-27T09:03:18Z","timestamp":1440666198000},"page":"31-45","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Decomposition Method for the Verification of a Real-Time Safety-Critical Protocol"],"prefix":"10.1007","author":[{"given":"Tam\u00e1s","family":"T\u00f3th","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andr\u00e1s","family":"V\u00f6r\u00f6s","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Istv\u00e1n","family":"Majzik","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,8,28]]},"reference":[{"issue":"2","key":"3_CR1","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. Theor. Comput. Sci. 126(2), 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"3_CR2","unstructured":"Bartha, T., V\u00f6r\u00f6s, A., J\u00e1mbor, A., Darvas, D.: Verification of an industrial safety function using coloured petri nets and model checking. In: Proceedings of the 14th International Conference on Modern Information Technology in the Innovation Processes of the Industrial Entreprises (MITIP 2012), pp. 472\u2013485. Hungarian Academy of Sciences, Computer and Automation Research Institute (MTA SZTAKI) (2012)"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Behrmann, G., David, A., Larsen, K., Hakansson, J., Petterson, P., Yi, W., Hendriks, M.: Uppaal 4.0. In: Third International Conference on Quantitative Evaluation of Systems (QEST 2006), pp. 125\u2013126 (2006)","DOI":"10.1109\/QEST.2006.59"},{"key":"3_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-540-27755-2_3","volume-title":"Lectures on Concurrency and Petri Nets","author":"JE Bengtsson","year":"2004","unstructured":"Bengtsson, J.E., Yi, W.: Timed automata: semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets. LNCS, vol. 3098, pp. 87\u2013124. Springer, Heidelberg (2004)"},{"key":"3_CR5","volume-title":"Model Checking","author":"EM Clarke Jr","year":"1999","unstructured":"Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"3_CR6","series-title":"Lecture Notes in Computer Science","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P D\u2018Argenio","year":"1997","unstructured":"D\u2018Argenio, P., Katoen, J.P., Ruys, T., Tretmans, J.: The bounded retransmission protocol must be on time!. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol. 1217. Springer, Heidelberg (1997)"},{"key":"3_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/978-3-642-15898-8_9","volume-title":"Formal Methods for Industrial Critical Systems","author":"M Gerke","year":"2010","unstructured":"Gerke, M., Ehlers, R., Finkbeiner, B., Peter, H.-J.: Model checking the FlexRay physical layer protocol. In: Kowalewski, S., Roveri, M. (eds.) FMICS 2010. LNCS, vol. 6371, pp. 132\u2013147. Springer, Heidelberg (2010)"},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"414","DOI":"10.1007\/978-3-642-02658-4_32","volume-title":"Computer Aided Verification","author":"R Kaivola","year":"2009","unstructured":"Kaivola, R., Ghughal, R., Narasimhan, N., Telfer, A., Whittemore, J., Pandav, S., Slobodov\u00e1, A., Taylor, C., Frolov, V., Reeber, E., Naik, A.: Replacing testing with formal verification in Intel CoreTM i7 processor execution engine validation. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 414\u2013429. Springer, Heidelberg (2009)"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Pike, L.: Modeling time-triggered protocols and verifying their real-time schedules. In: Formal Methods in Computer Aided Design (FMCAD 2007), pp. 231\u2013238 (2007)","DOI":"10.1109\/FAMCAD.2007.10"},{"key":"3_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/978-3-642-19835-9_32","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"AP Ravn","year":"2011","unstructured":"Ravn, A.P., Srba, J., Vighio, S.: Modelling and verification of web services business activity protocol. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 357\u2013371. Springer, Heidelberg (2011)"},{"key":"3_CR11","series-title":"Advances in Intelligent Systems and Computing","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1007\/978-3-319-00945-2_43","volume-title":"New Results in Dependability and Computer Systems","author":"T T\u00f3th","year":"2013","unstructured":"T\u00f3th, T., V\u00f6r\u00f6s, A., Istv\u00e1n, M.: K-induction based verification of real-time safety critical systems. New Results in Dependability and Computer Systems. AISC, vol. 224, pp. 469\u2013478. Springer International Publishing, Switzerland (2013)"}],"container-title":["Lecture Notes in Computer Science","Software Engineering for Resilient Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-23129-7_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T05:34:07Z","timestamp":1748583247000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-23129-7_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319231280","9783319231297"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-23129-7_3","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":"28 August 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}