{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,2]],"date-time":"2025-03-02T05:46:36Z","timestamp":1740894396628,"version":"3.38.0"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540204619"},{"type":"electronic","value":"9783540398936"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-39893-6_30","type":"book-chapter","created":{"date-parts":[[2011,1,7]],"date-time":"2011-01-07T15:35:57Z","timestamp":1294414557000},"page":"523-540","source":"Crossref","is-referenced-by-count":4,"title":["Verification of Timeliness QoS Properties in Multimedia Systems"],"prefix":"10.1007","author":[{"given":"Behzad","family":"Bordbar","sequence":"first","affiliation":[]},{"given":"Kozo","family":"Okano","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"unstructured":"Akehurst, D.H., Bordbar, B., Derrick, J., Waters, A.G.: Design support for distributed systems: dse4ds. In: Finney, J., Haahr, M., Montressor, A. (eds.) Proceedings of the 7th Cabernet Radicals Workshop (October 2002)","key":"30_CR1"},{"key":"30_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/978-3-540-49382-2_22","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"L. Ageto","year":"1998","unstructured":"Ageto, L., Bouyer, P., Burgue\u00f1o, A., Larsen, K.G.: The Power of Reachability Testing for Timed Automata. In: Arvind, V., Sarukkai, S. (eds.) FST TCS 1998. LNCS, vol.\u00a01530, pp. 245\u2013256. Springer, Heidelberg (1998)"},{"doi-asserted-by":"crossref","unstructured":"Ageto, L., Bouyer, P., Burgue\u00f1o, A., Larsen, K.G.: Model-Checking via Reachability Testing for Timed Automata. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.\u00a01384, pp. 263\u2013280. Springer, Heidelberg (1998)","key":"30_CR3","DOI":"10.1007\/BFb0054177"},{"doi-asserted-by":"crossref","unstructured":"Ageto, L., Bouyer, P., Burgue\u00f1o, A., Larsen, K.G.: The Power of Reachability Testing for Timed Automata, Available from http:\/\/www.lsv.ens-cachan.fr\/Publis\/publis-y3-2003.php (to appear in Theoretical Computer Science)","key":"30_CR4","DOI":"10.1016\/S0304-3975(02)00334-1"},{"key":"30_CR5","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"125","author":"R. Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A Theory for Timed Automata. Theoretical Computer Science\u00a0125, 183\u2013235 (1994)","journal-title":"Theoretical Computer Science"},{"key":"30_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1007\/3-540-45510-8_4","volume-title":"Modeling and Verification of Parallel Processes","author":"T. Amnell","year":"2001","unstructured":"Amnell, T., Behmann, G., Bengtsson, J., D\u2019Argenio, P.R., David, A., Fehnker, A., Hune, T., Jeannet, B., Larsen, K.G., M\u00f6ller, O., Pettersson, P., Weise, C., Yi, W.: UPPAAL\u2014Now, Next and Future. In: Cassez, F., Jard, C., Rozoy, B., Dermot, M. (eds.) MOVEP 2000. LNCS, vol.\u00a02067, pp. 100\u2013125. Springer, Heidelberg (2001)"},{"key":"30_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1007\/3-540-45800-X_22","volume-title":"\u00abUML\u00bb 2002 - The Unified Modeling Language. Model Engineering, Concepts, and Tools","author":"J. \u00d8yvind Aagedal","year":"2002","unstructured":"\u00d8yvind Aagedal, J., Ecklund Jr, E.F.: Modelling QoS: Towards a UML Profile. In: J\u00e9z\u00e9quel, J.-M., Hussmann, H., Cook, S. (eds.) UML 2002. LNCS, vol.\u00a02460, pp. 275\u2013289. Springer, Heidelberg (2002)"},{"key":"30_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1007\/3-540-61474-5_73","volume-title":"Computer Aided Verification","author":"J. Bengtsson","year":"1996","unstructured":"Bengtsson, J., Griffioen, W.O.D., Kristoffersen, K.J., Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: Verification of an Audio Protocol with Bus Collision Using UPPAAL. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 244\u2013256. Springer, Heidelberg (1996)"},{"doi-asserted-by":"crossref","unstructured":"Bengtsson, J., Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: UPPAAL, a Tool suite for automatic verification of real-time systems. In: Proceedings of Workshop on Hybrid Systems III: Verification and Control. LNCS, vol.\u00a01066, pp. 232\u2013243 (1995)","key":"30_CR9","DOI":"10.1007\/BFb0020949"},{"key":"30_CR10","volume-title":"Open Distributed Processing and Multimedia","author":"G. Blair","year":"1997","unstructured":"Blair, G., Stefani, J.-B.: Open Distributed Processing and Multimedia. Addison-Wesley, Boston (1997)"},{"key":"30_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"561","DOI":"10.1007\/3-540-36103-0_56","volume-title":"Formal Methods and Software Engineering","author":"B. Bordbar","year":"2002","unstructured":"Bordbar, B., Derrick, J., Waters, A.G.: A UML approach to the design of open distributed systems. In: George, C.W., Miao, H. (eds.) ICFEM 2002. LNCS, vol.\u00a02495, pp. 561\u2013572. Springer, Heidelberg (2002)"},{"doi-asserted-by":"crossref","unstructured":"Bordbar, B., Derrick, J., Waters, A.G.: Using UML to specify QoS constraints. In: ODP Computer network and ISDN systems, vol.\u00a040, pp. 279\u2013304 (2002)","key":"30_CR12","DOI":"10.1016\/S1389-1286(02)00255-4"},{"key":"30_CR13","first-page":"261","volume-title":"Proceedings of Design, Specification and Verification of Interactive Systems 1998","author":"H. Bowman","year":"1998","unstructured":"Bowman, H., Faconti, G., Massink, M.: Specification and verification of media constraints using UPPAAL. In: Markopoulos, Johnos, P. (eds.) Proceedings of Design, Specification and Verification of Interactive Systems 1998, pp. 261\u2013277. Springer, Heidelberg (1998)"},{"doi-asserted-by":"crossref","unstructured":"Havelund, K., Skou, A., Larsen, K.G., Lund, K.: 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, pp. 2\u201313 (1997)","key":"30_CR14","DOI":"10.7146\/brics.v4i31.18957"},{"unstructured":"J\u00e9z\u00e9quel, J.-M.: Model-driven engineering with contracts, patterns, and aspects. In: Tutorial Program of AOSD 2003: 2nd International Conference on Aspect-Oriented Software Development. ACM-IEEE (March 2003)","key":"30_CR15"},{"doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a Nutshell. Springer International Journal of Software Tools for Technology Transfer\u00a01(1+2) (1997)","key":"30_CR16","DOI":"10.1007\/s100090050010"},{"issue":"3","key":"30_CR17","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/s100090100048","volume":"3","author":"M. Lindahl","year":"2001","unstructured":"Lindahl, M., Pettersson, P., Yi, W.: Formal Design and Analysis of a Gear Controller. Springer International Journal of Software Tools for Technology Transfer\u00a03(3), 353\u2013368 (2001)","journal-title":"Springer International Journal of Software Tools for Technology Transfer"},{"doi-asserted-by":"crossref","unstructured":"L\u00f6nn, H., Pettersson, P.: Formal Verification of a TDMA Protocol Start-Up Mechanism. In: Proceedings of 1997 IEEE Pacific Rim International Symposium on Fault-Tolerant Systems, pp. 235\u2013242 (1997)","key":"30_CR18","DOI":"10.1109\/PRFTS.1997.640153"},{"unstructured":"Lorcy, S., Plouzeau, N., J\u00e9z\u00e9quel, J.-M.: Reifying quality of service contracts for distributed software. In: 26th Conference on Technology of Object- Oriented Systems (TOOLS USA 1998) (August 1998)","key":"30_CR19"},{"key":"30_CR20","volume-title":"Communication and concurrency","author":"R. Milner","year":"1989","unstructured":"Milner, R.: Communication and concurrency. Prentice Hall, Upper Saddle River (1989)"},{"unstructured":"ITU Recommendation X.901-904 ISO\/IEC 10746 1-4. Open Distributed Processing Reference Model - Parts 1-4 (July 1995)","key":"30_CR21"},{"unstructured":"Staehli, R., Eliassen, F., \u00d8yvind Aagedal, J., Blair, G.S.: Quality of Service Semantics for Component-Based Systems. In: The 1st International Workshop on Middleware for Grid Computing, pp. 153\u2013157 (2003)","key":"30_CR22"},{"key":"30_CR23","series-title":"Lecture Notes in Computer Science","first-page":"502","volume-title":"CONCUR \u201990","author":"W. Yi","year":"1990","unstructured":"Yi, W.: Real-Time Behaviour of Asynchronous Agents. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol.\u00a0458, pp. 502\u2013520. Springer, Heidelberg (1990)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-39893-6_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,1]],"date-time":"2025-03-01T14:26:19Z","timestamp":1740839179000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-39893-6_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540204619","9783540398936"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-39893-6_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}