{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,9]],"date-time":"2026-05-09T04:37:09Z","timestamp":1778301429137,"version":"3.51.4"},"reference-count":29,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2006,12,1]],"date-time":"2006-12-01T00:00:00Z","timestamp":1164931200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2006,12]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            The biphase mark protocol is a convention for representing both a string of bits and clock edges in a square wave. The protocol is frequently used for communication at the physical level of the ISO\/OSI hierarchy, and is implemented on microcontrollers such as the Intel 82530 Serial Communications Controller. An important property of the protocol is that bit strings of arbitrary length can be transmitted reliably, despite differences in the clock rates of sender and receiver (drift), variations of the clock rates (jitter), and distortion of the signal after generation of an edge. In this article, we show how the protocol can be modelled naturally in terms of timed automata. We use the model checker\n            <jats:sc>Uppaal<\/jats:sc>\n            to derive the maximal tolerances on the clock rates, for different instances of the protocol, and to support the general parametric verification that we formalized using the proof assistant PVS. Based on the derived parameter constraints we propose instances of BMP that are correct (at least in our model) but have a faster bit rate than the instances that are commonly implemented in hardware.\n          <\/jats:p>","DOI":"10.1007\/s00165-006-0008-1","type":"journal-article","created":{"date-parts":[[2006,9,7]],"date-time":"2006-09-07T06:34:36Z","timestamp":1157610876000},"page":"433-458","source":"Crossref","is-referenced-by-count":22,"title":["Analysis of a biphase mark protocol with U\n            <scp>ppaal<\/scp>\n            and PVS"],"prefix":"10.1145","volume":"18","author":[{"given":"F. W.","family":"Vaandrager","sequence":"first","affiliation":[{"name":"Institute for Computing and Information Sciences, Radboud University Nijmegen, Nijmegen, The Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A. L.","family":"de Groot","sequence":"additional","affiliation":[{"name":"Institute for Computing and Information Sciences, Radboud University Nijmegen, Nijmegen, The Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","first-page":"419","volume-title":"Proceedings of the 12th international conference on Computer aided verification, vol 1855 of Lecture Notes in Computer Science","author":"Annichini A","year":"2000"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_2_1_2_3_2","unstructured":"Advanced Micro Devices Inc (1992) Technical Manual Am8530H\/Am85C30 Serial Communications Controller"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Alur R Henzinger TA (eds) (1996) Proceedings of the 8th international conference on computer aided verification New Brunswick NJ USA vol 1102 of Lecture Notes in Computer Science . Springer Berlin Heidelberg New York","DOI":"10.1007\/3-540-61474-5"},{"key":"e_1_2_1_2_5_2","unstructured":"Myla Archer (1998) Constance Heitmeyer and Steve Sims. TAME: a PVS interface to simplify proofs for automata models. In: User interfaces for theorem Provers . Eindhoven The Netherlands"},{"key":"e_1_2_1_2_6_2","first-page":"58","volume-title":"SAS, vol 1824 of Lecture Notes in Computer Science","author":"Bensalem S","year":"2000"},{"key":"e_1_2_1_2_7_2","first-page":"546","volume-title":"Proceedings of the 10th international conference on computer aided verification, Vancouver, BC, Canada, vol 1427 of Lecture Notes in Computer Science","author":"Bozga M","year":"1998"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Bengtsson J Griffioen WOD Kristoffersen KJ Larsen KG Larsson F Pettersson P Yi W (1996) Verification of an audio protocol with bus collision using UPPAAL. In: Alur and Henzinger [Ah96] pp 244\u2013256","DOI":"10.1007\/3-540-61474-5_73"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Bensalem S Lakhnech Y Saidi H (1996) Powerful techniques for the automatic generation of invariants. In: Alur and Henzinger [AH86] pp 323\u2013335","DOI":"10.1007\/3-540-61474-5_80"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"publisher","DOI":"10.5555\/50756"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Bosscher DJB Polak I Vaandrager FW (1994) Verification of an audio control protocol. In: Langmaack H de Roever W-P Vytopil J (eds) Proceedings of the third international school and symposium on formal techniques in real-time and fault-tolerant systems (FTRTFT\u201994) L\u00fcbeck Germany September 1994 vol 863 of Lecture Notes in Computer Science Springer Berlin Heidelberg New York pp 170\u2013192","DOI":"10.1007\/3-540-58468-4_165"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Chkliaev D Hooman J de Vink E (2003) Verification and improvement of the sliding window protocol. In: Proceedings TACAS\u201903 vol 2619. Lecture Notes in Computer Science Springer Berlin Heidelberg New York pp 113\u2013127","DOI":"10.1007\/3-540-36577-X_9"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01784024"},{"key":"e_1_2_1_2_14_2","unstructured":"Collomb\u2013Annichini A Sighireanu M (2001) Parameterized reachability analysis of the IEEE 1394 Root Contention Protocol using TReX. In: Pettersson p Yovine S (eds) Proceedings of the Workshop on Real-Time Tools (RT-TOOLS\u20192001)"},{"key":"e_1_2_1_2_15_2","volume-title":"Microprocessor verification in PVS: a methodology and simple example","author":"Cyrluk D","year":"1993"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Daws C Yovine S (1995) Two examples of verification of multirate timed automata with kronos . In: Proceedings of the 16th IEEE real-time systems symposium (RTSS\u201995). Pisa Italy. IEEE Computer Society Press New York pp 66\u201375","DOI":"10.1109\/REAL.1995.495197"},{"key":"e_1_2_1_2_17_2","unstructured":"Griffioen WOD (2000) Studies in Computer Aided verification of protocols. PhD thesis University of Nijmegen May 2000. http:\/\/www.cs.kun.nl\/ita\/former_members\/davidg\/ IPA thesis no. 2000-04"},{"key":"e_1_2_1_2_18_2","unstructured":"Hung DV Kwang K II (1996) Verification via digitized models of real-time hybrid systems. In: Proceedings Asia-Pacific software engineering conference (APSEC\u201996). IEEE Computer Society Press New York pp 4\u201315"},{"key":"e_1_2_1_2_19_2","unstructured":"Henzinger TA Preussig J Wong-Toi H (2001) Some lessons from the HyTech experience. In: Proceedings of the 40th Annual Conference on Decision and Control (CDC) . IEEE Press New York pp 2887\u20132892"},{"issue":"53","key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/S1567-8326(02)00037-1","article-title":"Linear parametric model checking of timed automata","volume":"52","author":"Hune TS","year":"2002","journal-title":"J Logic Algebraic Program"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Havelund K Skou A Larsen KG Lund K (1997) Formal modelling and analysis of an audio\/video protocol: an industrial case study using Uppaal . In: Proceedings of the 18th IEEE real-time systems symposium . IEEE Computer Society Press New York pp 2\u201313","DOI":"10.7146\/brics.v4i31.18957"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Hung DV (1998) Modelling and verification of biphase mark protocols using PVS. In: Proceedings of the international conference on applications of concurrency to system design (CSD\u201998) Aizu-wakamatsu Fukushima Japan March 1998. IEEE Computer Society Press pp 88\u201398","DOI":"10.1109\/CSD.1998.657542"},{"key":"e_1_2_1_2_23_2","volume-title":"Proceedings of the 7th international conference on computer aided verification, Li\u00e8ge, Belgium, vol 939 of Lecture Notes in Computer Science","author":"Ho P-H","year":"1995"},{"key":"e_1_2_1_2_24_2","unstructured":"Ivanov S Griffioen WOD (1999) Verification of a biphase mark protocol. Report CSI-R9915 Computing Science Institute University of Nijmegen August 1999"},{"key":"e_1_2_1_2_25_2","unstructured":"Intel Corporation. Microcommunications (1991) Intel Literature Sales P.O. Box 7641 Mt. Prospect IL 60056-7641"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050010"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Moore J.S[trother] (1994) A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocol. Formal Aspects Comput 6(1):60\u201391","DOI":"10.1007\/BF01211081"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.345827"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Sawada J Hunt WA (1998) Processor verification with precise exceptions and speculative execution. In: Proceedings of 10th international computer aided verification conference pp 135\u2013146","DOI":"10.1007\/BFb0028740"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-006-0008-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-006-0008-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-006-0008-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:44:52Z","timestamp":1641483892000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-006-0008-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,12]]},"references-count":29,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2006,12]]}},"alternative-id":["10.1007\/s00165-006-0008-1"],"URL":"https:\/\/doi.org\/10.1007\/s00165-006-0008-1","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,12]]}}}