{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T15:02:39Z","timestamp":1694617359520},"reference-count":20,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[1998,4,1]],"date-time":"1998-04-01T00:00:00Z","timestamp":891388800000},"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,4]]},"abstract":"<jats:title>Abstract.<\/jats:title>\n          <jats:p>The PREMO standard, Presentation Environment for Multimedia Objects, is a major new standard under development within ISO\/IEC. It addresses the creation of, presentation of, and interaction with all forms of information using single or multiple media. In this paper we give a formal LOTOS specification, amenable to automatic verification, of the PREMO synchronisable object, which is one of the central parts of the standard. Various design options are investigated by a combination of constraint oriented specification and model checking. This shows the usefulness of formal specification and automatic verification during the design phase of an international standard.<\/jats:p>","DOI":"10.1007\/s001650050024","type":"journal-article","created":{"date-parts":[[2002,8,25]],"date-time":"2002-08-25T07:30:30Z","timestamp":1030260630000},"page":"405-434","source":"Crossref","is-referenced-by-count":0,"title":["Modelling and Verification of PREMO Synchronisable Objects"],"prefix":"10.1145","volume":"10","author":[{"given":"G. P.","family":"Faconti","sequence":"first","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, , , , , , GB"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"p_1","volume-title":"Proceedings Workshop on Automated Formal Methods, ENTCS","volume":"5","author":"Be","year":"1996"},{"key":"p_2","volume-title":"et al.: Proof in VDM: A Practitioner\u2019s Guide","author":"Bic","year":"1994"},{"key":"p_3","first-page":"207","volume":"54","author":"Bouali A.","year":"1994","journal-title":"The Integration Project for the JACK Environment. Bulletin of the EATCS"},{"key":"p_4","volume-title":"Proceedings of the 5th Eurographics Workshop on the Design, Specification and Verification of Interactive Systems, DSV-IS 98","author":"Bowman H.","year":"1998"},{"key":"p_6","volume-title":"Proceedings 3rd International Workshop CAV'91","author":"De Nicola R.","year":"1991"},{"key":"p_7","first-page":"246","volume-title":"Proceedings of CHARME'95","author":"De Nicola R.","year":"1995"},{"issue":"2","key":"p_8","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1007\/BF01213486","volume":"1","author":"Dannemberg R. B.","year":"1993","journal-title":"Multimedia System Journal"},{"key":"p_12","volume-title":"Granada","author":"Fa","year":"1997"},{"key":"p_13","volume-title":"Electronic Workshops in Computing, proceedings of the BCS-FACS Second Northern Formal Methods Workshop","author":"Fa","year":"1997"},{"key":"p_14","volume-title":"Communications of ACM, 21(8)","author":"Hoa","year":"1978"},{"key":"p_15","first-page":"8807","author":"[ISO89] International Standards Organization ISO. Information processing systems, open systems interconnection, LOTOS. A formal description technique based on the temporal ordering of observational behaviour.","year":"1989","journal-title":"ISO"},{"key":"p_16","first-page":"14478","author":"[ISO96] International Standards Organization ISO. Information processing systems, computer graphics, presentation environment for multimedia objects (PREMO).","year":"1996","journal-title":"ISO\/IEC"},{"issue":"1","key":"p_17","volume":"1","author":"Larsen G.","year":"1997","journal-title":"Journal of Software Tools for Technology Transfer"},{"key":"p_18","first-page":"61","volume-title":"II","author":"Ma","year":"1990"},{"key":"p_19","series-title":"Series in Computer Science","volume-title":"Communication and Concurrency","author":"Mil","year":"1989"},{"key":"p_21","first-page":"65","volume-title":"Proceedings Workshop on Computer Aided Verification, LNCS 531","author":"Roy V.","year":"1990"},{"key":"p_22","volume-title":": The Z Notation: A Reference Manual","author":"Spi","year":"1989"},{"issue":"1","key":"p_23","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1109\/49.481694","volume":"14","author":"Ste","year":"1996","journal-title":"IEEE Journal on Selected Areas in Communications"},{"key":"p_24","volume-title":"Proceedings of 4th Int. Conference on Formal Description Techniques. North Holland","author":"Ei","year":"1991"},{"key":"p_25","volume-title":"van and Brinksma","author":"Vissers C. A.","year":"1991"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s001650050024.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s001650050024\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s001650050024","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:27:26Z","timestamp":1641482846000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s001650050024"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998,4]]},"references-count":20,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1998,4]]}},"alternative-id":["10.1007\/s001650050024"],"URL":"https:\/\/doi.org\/10.1007\/s001650050024","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1998,4]]}}}