{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:45:16Z","timestamp":1725561916275},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540212997"},{"type":"electronic","value":"9783540247302"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24730-2_29","type":"book-chapter","created":{"date-parts":[[2010,8,2]],"date-time":"2010-08-02T11:00:15Z","timestamp":1280746815000},"page":"372-387","source":"Crossref","is-referenced-by-count":2,"title":["Automatic Parametric Verification of a Root Contention Protocol Based on Abstract State Machines and First Order Timed Logic"],"prefix":"10.1007","author":[{"given":"Dani\u00e8le","family":"Beauquier","sequence":"first","affiliation":[]},{"given":"Tristan","family":"Crolard","sequence":"additional","affiliation":[]},{"given":"Evguenia","family":"Prokofieva","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"29_CR1","unstructured":"Bandini, G., Lutje Spelberg, R.L., de Rooij, R.C.H., Toetenel, W.J.: Application of parametric model checking - the root contention protocol. In: Sixth Annual Conference of the Advanced School for Computing and Imaging (ASCI 2000), Lommel, Belgium (June 2000)"},{"key":"29_CR2","unstructured":"Beauquier, D., Slissenko, A.: On semantics of algorithms with continuous time. Technical Report 97\u201315, Revised version., University Paris 12, Department of Informatics (1997), Available at http:\/\/www.eecs.umich.edu\/gasm\/ and at http:\/\/www.univparis12.fr\/lacl\/"},{"issue":"1-3","key":"29_CR3","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1016\/S0168-0072(01)00049-5","volume":"113","author":"D. Beauquier","year":"2002","unstructured":"Beauquier, D., Slissenko, A.: A first order logic for specification of timed algorithms: Basic properties and a decidable class. Annals of Pure and Applied Logic\u00a0113(1-3), 13\u201352 (2002)","journal-title":"Annals of Pure and Applied Logic"},{"key":"29_CR4","unstructured":"Beauquier, D., Crolard T., Prokofieva E.: Automatic verification of real time systems: A case study. In: Third Workshop on Automated Verification of Critical Systems (AVoCS 2003), Technical Report of the University of Southampton, pp. 98\u2013108, Southampton (UK) (April 2003)"},{"key":"29_CR5","unstructured":"Collomb-Annichini, A., Sighireanu, M.: Parametrized reachability analysis of the IEEE 1394 root contention protocol using TReX. In: Proceedings of the Workshop on Real-Time Tools, RT-TOOLS 2001 (2001)"},{"key":"29_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"266","DOI":"10.1007\/3-540-61377-3_43","volume-title":"Computer Science Logic","author":"Y. Gurevich","year":"1996","unstructured":"Gurevich, Y., Huggins, J.: The railroad crossing problem: an experiment with instantaneous actions and immediate reactions. In: Kleine B\u00fcning, H. (ed.) CSL 1995. LNCS, vol.\u00a01092, pp. 266\u2013290. Springer, Heidelberg (1996)"},{"key":"29_CR7","first-page":"9","volume-title":"Specification and Validation Methods","author":"Y. Gurevich","year":"1995","unstructured":"Gurevich, Y.: Evolving algebra 1993: Lipari guide. In: B\u00f6rger, E. (ed.) Specification and Validation Methods, pp. 9\u201393. Oxford University Press, Oxford (1995)"},{"key":"29_CR8","unstructured":"Hearn, A.C.: Reduce user\u2019s and contributed packages manual, version 3.7. Available from Konrad-Zuse-Zentrum Berlin, Germany (February 1999), http:\/\/www.uni-koeln.de\/REDUCE\/"},{"key":"29_CR9","doi-asserted-by":"crossref","unstructured":"Hune, T.S., Romijn, J.M.T., Stoelinga, M.I.A., Vaandrager, F.W.: Linear parametric model checking of timed automata. Journal of Logic and Algebraic Programming (2002)","DOI":"10.1016\/S1567-8326(02)00037-1"},{"key":"29_CR10","unstructured":"Stoelinga, M.I.A.: Fun with FireWire: Experiments with verifying the IEEE 1394 root contention protocol. In: Romijn, J.M.T., Maharaj, S., Shankland, C. (eds.) Formal Aspects of Computing (2002) (accepted for publication)"},{"key":"29_CR11","doi-asserted-by":"crossref","unstructured":"Stoelinga, M.I.A., Vaandrager, F.W.: Root contention in IEEE 1394, Bamberg, Germany, May 1999, pp. 53\u201375 (1999)","DOI":"10.1007\/3-540-48778-6_4"},{"key":"29_CR12","doi-asserted-by":"crossref","unstructured":"Toetenel, H., Spelberg, R.L., Bandini, G.: Parametric verification of the IEEE 1394a root contention protocol using LPMC. In: Seventh International Conference on Real-Time Systems and Applications (RTCSA 2000), Cheju Island, South Korea (December 2000)","DOI":"10.1109\/RTCSA.2000.896393"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24730-2_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T23:18:30Z","timestamp":1559344710000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24730-2_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540212997","9783540247302"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24730-2_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}