{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:26:56Z","timestamp":1742912816626,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642043673"},{"type":"electronic","value":"9783642043680"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-04368-0_20","type":"book-chapter","created":{"date-parts":[[2009,9,2]],"date-time":"2009-09-02T03:31:59Z","timestamp":1251862319000},"page":"258-274","source":"Crossref","is-referenced-by-count":1,"title":["Machine-Assisted Parameter Synthesis of the Biphase Mark Protocol Using Event Order Abstraction"],"prefix":"10.1007","author":[{"given":"Shinya","family":"Umeno","sequence":"first","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"20_CR1","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/BF01211081","volume":"6","author":"J.S. Moore","year":"1994","unstructured":"Moore, J.S.: A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocol. Formal Aspects of Computing\u00a06(1), 60\u201391 (1994)","journal-title":"Formal Aspects of Computing"},{"key":"20_CR2","doi-asserted-by":"crossref","unstructured":"Umeno, S.: Event order abstraction for parametric real-time system verification. In: EMSOFT 2008: The 8th ACM & IEEE International Conference on Embedded Software, 1\u201310 (2008) A technical report version appears as MIT-CSAIL-TR-2008-048, Massachusetts Institute of Technology (July 2008)","DOI":"10.1145\/1450058.1450060"},{"issue":"4","key":"20_CR3","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1007\/s00165-006-0008-1","volume":"18","author":"F.W. Vaandrager","year":"2006","unstructured":"Vaandrager, F.W., de Groot, A.: Analysis of a biphase mark protocol with UPPAAL and PVS. Formal Asp. Comput.\u00a018(4), 433\u2013458 (2006)","journal-title":"Formal Asp. Comput."},{"key":"20_CR4","unstructured":"Zhang, D., Cleaveland, R.: Fast on-the-fly parametric real-time model checking. In: Proceedings of the 26th IEEE Real-Time Systems Symposium, pp. 157\u2013166 (2005)"},{"key":"20_CR5","volume-title":"Distributed Algorithms","author":"N.A. Lynch","year":"1996","unstructured":"Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann Publishers Inc., San Francisco (1996)"},{"key":"20_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/11691372_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G.M. Brown","year":"2006","unstructured":"Brown, G.M., Pike, L.: Easy parameterized verification of biphase mark and 8N1 protocols. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 58\u201372. Springer, Heidelberg (2006)"},{"key":"20_CR7","first-page":"2887","volume-title":"Proc. of the 40th Annual Conference on Decision and Control","author":"T. Henzinger","year":"2001","unstructured":"Henzinger, T., Preussig, J., Wong-Toi, H.: Some lessons from the HYTECH experience. In: Proc. of the 40th Annual Conference on Decision and Control, pp. 2887\u20132892. IEEE Computer Society Press, Los Alamitos (2001)"},{"key":"20_CR8","unstructured":"Ivanov, S., Griffioen, W.: Verification of a biphase mark protocol. Technical report (1999)"},{"key":"20_CR9","doi-asserted-by":"crossref","unstructured":"Hune, T., Romijn, J., Stoelinga, M., Vaandrager, F.W.: Linear parametric model checking of timed automata. In: Tools and Algorithms for Construction and Analysis of Systems, pp. 189\u2013203 (2001)","DOI":"10.1007\/3-540-45319-9_14"},{"key":"20_CR10","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1109\/TSE.2005.13","volume":"31","author":"F. Wang","year":"2005","unstructured":"Wang, F.: Symbolic parametric safety analysis of linear hybrid systems with BDD-like data-structures. Transactions on Software Engineering\u00a031, 38\u201351 (2005)","journal-title":"Transactions on Software Engineering"},{"key":"20_CR11","doi-asserted-by":"crossref","unstructured":"Annichini, A., Bouajjani, A., Sighireanu, M.: TReX: A tool for reachability analysis of complex systems. In: Computer Aided Verification, pp. 368\u2013372 (2001)","DOI":"10.1007\/3-540-44585-4_34"},{"key":"20_CR12","first-page":"88","volume":"8","author":"R. Spelberg","year":"2001","unstructured":"Spelberg, R., Toetenel, W.: Parametric real-time model checking using splitting trees. Nordic Journal of Computing\u00a08, 88\u2013120 (2001)","journal-title":"Nordic Journal of Computing"},{"key":"20_CR13","unstructured":"Collomb-Annichini, A., Sighireanu, M.: Parameterized reachability analysis of the ieee 1394 root contention protocol using trex. In: RT-TOOL 2001 (2001)"},{"key":"20_CR14","doi-asserted-by":"crossref","DOI":"10.21236\/ADA262848","volume-title":"The Temporal Logic of Reactive and Concurent Systems: Specification","author":"Z. Manna","year":"1993","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurent Systems: Specification. Springer, Heidelberg (1993)"},{"key":"20_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"496","DOI":"10.1007\/978-3-540-27813-9_45","volume-title":"Computer Aided Verification","author":"L.M. Moura de","year":"2004","unstructured":"de Moura, L.M., Owre, S., Rue\u00df, H., Rushby, J.M., Shankar, N., Sorea, M., Tiwari, A.: SAL 2. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 496\u2013500. Springer, Heidelberg (2004)"},{"key":"20_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction - CADE-11","author":"S. Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607, pp. 748\u2013752. Springer, Heidelberg (1992)"},{"key":"20_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/11813040_5","volume-title":"FM 2006: Formal Methods","author":"S. Umeno","year":"2006","unstructured":"Umeno, S., Lynch, N.A.: Proving safety properties of an aircraft landing protocol using I\/O automata and the PVS theorem prover: A case study. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol.\u00a04085, pp. 64\u201380. Springer, Heidelberg (2006)"},{"key":"20_CR18","unstructured":"Dutertre, B., Sorea, M.: Timed systems in SAL. Technical Report SRI-SDL-04-03, SRI International (2004)"},{"key":"20_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-540-30206-3_15","volume-title":"Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems","author":"B. Dutertre","year":"2004","unstructured":"Dutertre, B., Sorea, M.: Modeling and verification of a fault-tolerant real-time startup protocol using calendar automata. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS 2004 and FTRTFT 2004. LNCS, vol.\u00a03253, pp. 199\u2013214. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Formal Modeling and Analysis of Timed Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-04368-0_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,9]],"date-time":"2019-03-09T11:57:45Z","timestamp":1552132665000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-04368-0_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642043673","9783642043680"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-04368-0_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}