{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,4]],"date-time":"2025-10-04T08:14:02Z","timestamp":1759565642728},"reference-count":22,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[1998,5,1]],"date-time":"1998-05-01T00:00:00Z","timestamp":893980800000},"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":[[1998,5]]},"abstract":"<jats:title>Abstract.<\/jats:title>\n          <jats:p>We present the formal specification and verification of a             lip-synchronisation protocol using the real-time model checker Uppaal. A number of specifications of this protocol can be found in the literature, but this is the first automatic verification. We take a published specification of the protocol, code it up in the Uppaal timed automata notation and then verify whether the protocol satisfies the key properties of jitter and skew. The verification reveals some aws in the protocol. In particular, it shows that for certain sound and video streams the protocol can time-lock before reaching a prescribed error state. We also discuss our experience with Uppaal, with particular reference to modelling timeouts and to deadlock analysis.<\/jats:p>","DOI":"10.1007\/s001650050032","type":"journal-article","created":{"date-parts":[[2002,8,25]],"date-time":"2002-08-25T07:30:30Z","timestamp":1030260630000},"page":"550-575","source":"Crossref","is-referenced-by-count":26,"title":["Automatic Verification of a Lip-Synchronisation Protocol Using Uppaal"],"prefix":"10.1145","volume":"10","author":[{"given":"H.","family":"Bowman","sequence":"first","affiliation":[{"name":"Computing Laboratories, University of Kent at Canterbury, Kent, UK, , , , , , UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"G.","family":"Faconti","sequence":"additional","affiliation":[{"name":"CNR-Istituto CNUCE, Pisa, Italy, , , , , , IT"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J.-P.","family":"Katoen","sequence":"additional","affiliation":[{"name":"Informatik VII, U. of Erlangen-N\u00fcrnberg, Erlangen, Germany, , , , , , DE"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"D.","family":"Latella","sequence":"additional","affiliation":[{"name":"CNR-Istituto CNUCE, Pisa, Italy, , , , , , IT"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M.","family":"Massink","sequence":"additional","affiliation":[{"name":"Dept. of Computer Science, University of York, York, UK, , , , , , UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"p_1","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","article-title":"A theory of timed automata","volume":"126","author":"Al","year":"1994","journal-title":"Th. Comp. Sci."},{"key":"p_2","first-page":"244","volume-title":"Alur, R. and Henzinger, T. A., eds, Computer-Aided Verification VIII, LNCS 1102","author":"Bengtsson J.","year":"1996"},{"key":"p_3","volume-title":"Chetwynd","author":"Blair G. S.","year":"1997"},{"key":"p_4","first-page":"145","article-title":"A formal description technique supporting expression of quality of service and media synchronisation. In Hutchison, D., Danthine, A., Leopold, H., and Coulson, G., eds, Multimedia Transport and Teleservices","volume":"882","author":"Bowman H.","year":"1994","journal-title":"LNCS"},{"key":"p_5","series-title":"Computer Science Series","first-page":"261","volume-title":"Markopoulos, P. and Johnson, P., eds, Design, Specification and Verification of Interactive Systems","author":"Bowman H.","year":"1998"},{"key":"p_6","first-page":"110","volume-title":"Jonsson, B. and Parrow, J., eds, Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"Da","year":"1996"},{"key":"p_7","first-page":"126","volume-title":"Gries, D. and de Roever, W.-P., eds, Programming Concepts and Methods","author":"D\u2019Argenio P. R.","year":"1998"},{"key":"p_8","first-page":"416","volume-title":"E., ed, Tools and Algorithms for the Construction and Analysis of Systems, LNCS 1217","author":"D\u2019Argenio P. R.","year":"1997"},{"key":"p_9","first-page":"208","volume-title":"Alur, R., Henzinger, T. A., and Sontag, E. D., eds, Hybrid Systems III, LNCS 1066","author":"Daws C.","year":"1996"},{"key":"p_10","doi-asserted-by":"crossref","first-page":"126","DOI":"10.1109\/49.481699","article-title":"Using timed CSP for specification, verification and simulation of multimedia synchronization","volume":"14","author":"Feyzi Ates A.","year":"1996","journal-title":"IEEE J. on Sel. Areas in Comm."},{"issue":"9","key":"p_11","first-page":"901","article-title":"Formal methods for broadband and multimedia systems","volume":"30","author":"Fi","year":"1998","journal-title":"Comp. Netw. and ISDN Sys."},{"key":"p_12","first-page":"1","volume-title":"Proc. of the 2nd SPIN Workshop, Rutgers DIMACS Series","author":"Jensen H. E.","year":"1996"},{"issue":"1","key":"p_13","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/s100090050010","article-title":"Uppaal in a nutshell","volume":"1","author":"Larsen K. G.","year":"1997","journal-title":"Int. J. on Software Tools for Technology Transfer"},{"key":"p_14","first-page":"15","volume-title":"Proc. IFIP TC6 Int. Conf. on Open Distributed Processing","author":"Lin","year":"1995"},{"key":"p_15","volume-title":"Communication and Concurrency","author":"Mil","year":"1989"},{"key":"p_16","first-page":"526","volume-title":"J. W., Huizing, C., de Roever, W.-P., and Rozenberg, G., eds, Real-Time: Theory and Practice, LNCS 600","author":"Ni","year":"1991"},{"key":"p_17","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1007\/3-540-58179-0_45","volume-title":"Dill, D. L., ed, Computer Aided Verification VI, LNCS 818","author":"Olivero A.","year":"1994"},{"key":"p_18","volume-title":"Danthine, A., and Leduc, G., eds, Protocol Specification","author":"Reg","year":"1993"},{"issue":"2","key":"p_19","doi-asserted-by":"crossref","first-page":"114","DOI":"10.1016\/0140-3664(92)90131-W","article-title":"Computational model for distributed multimedia applications based on a synchronous programming language","volume":"15","author":"Stefani J.-B.","year":"1992","journal-title":"Comp. Comm."},{"issue":"1","key":"p_20","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1109\/49.481694","article-title":"Human perception of jitter and media synchronization","volume":"14","author":"Ste","year":"1996","journal-title":"IEEE J. on Sel. Areas in Comm."},{"key":"p_21","volume-title":"Hogrefe, D., and Leue, S., eds","author":"Wang Yi","year":"1994"},{"key":"p_22","volume-title":"Personal communication","author":"Yi","year":"1998"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s001650050032.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s001650050032\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s001650050032","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:28:15Z","timestamp":1641482895000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s001650050032"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998,5]]},"references-count":22,"journal-issue":{"issue":"5","published-print":{"date-parts":[[1998,5]]}},"alternative-id":["10.1007\/s001650050032"],"URL":"https:\/\/doi.org\/10.1007\/s001650050032","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1998,5]]}}}