{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T10:30:08Z","timestamp":1742380208693},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540212997"},{"type":"electronic","value":"9783540247302"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24730-2_26","type":"book-chapter","created":{"date-parts":[[2010,8,2]],"date-time":"2010-08-02T15:00:15Z","timestamp":1280761215000},"page":"327-341","source":"Crossref","is-referenced-by-count":14,"title":["A Scalable Incomplete Test for the Boundedness of UML RT Models"],"prefix":"10.1007","author":[{"given":"Stefan","family":"Leue","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Richard","family":"Mayr","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wei","family":"Wei","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"26_CR1","volume-title":"LICS 1993","author":"P. Abdulla","year":"1993","unstructured":"Abdulla, P., Jonsson, B.: Verifying Programs with Unreliable Channels. In: LICS 1993, IEEE, Los Alamitos (1993)"},{"issue":"1","key":"26_CR2","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1006\/inco.1996.0083","volume":"130","author":"P. Abdulla","year":"1996","unstructured":"Abdulla, P., Jonsson, B.: Undecidable verification problems for programs with unreliable channels. Information and Computation\u00a0130(1), 71\u201390 (1996)","journal-title":"Information and Computation"},{"key":"26_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_23","volume-title":"Computer Aided Verification","author":"R. Alur","year":"2000","unstructured":"Alur, R., Grosu, R., McDougall, M.: Efficient reachability analysis of hierarchical reactive machines. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, Springer, Heidelberg (2000)"},{"key":"26_CR4","volume-title":"Software Architecture in Practice","author":"L. Bass","year":"1998","unstructured":"Bass, L., Clements, P., Kazman, R.: Software Architecture in Practice. Addison-Wesley, Reading (1998)"},{"key":"26_CR5","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"B. Boigelot","year":"1996","unstructured":"Boigelot, B., Goidefroid, P.: Symbolic verification of communication protocols with infinite state spaces using qdds. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, Springer, Heidelberg (1996)"},{"key":"26_CR6","series-title":"Lecture Notes in Computer Science","volume-title":"Automata, Languages and Programming","author":"A. Bouajjani","year":"1997","unstructured":"Bouajjani, A., Habermehl, P.: Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) ICALP 1997. LNCS, vol.\u00a01256, Springer, Heidelberg (1997)"},{"key":"26_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/3-540-49116-3_30","volume-title":"STACS 99","author":"A. Bouajjani","year":"1999","unstructured":"Bouajjani, A., Mayr, R.: Model checking lossy vector addition systems. In: Meinel, C., Tison, S. (eds.) STACS 1999. LNCS, vol.\u00a01563, p. 323. Springer, Heidelberg (1999)"},{"issue":"5","key":"26_CR8","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1145\/322374.322380","volume":"2","author":"D. Brand","year":"1983","unstructured":"Brand, D., Zafiropulo, P.: On communicating finite-state machines. Journal of the ACM\u00a02(5), 323\u2013342 (1983)","journal-title":"Journal of the ACM"},{"issue":"1","key":"26_CR9","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/BF01384316","volume":"6","author":"J.C. Corbett","year":"1995","unstructured":"Corbett, J.C., Avrunin, G.S.: Using integer programming to verify general safety and liveness properties. Formal Methods in System Design: An International Journal\u00a06(1), 97\u2013123 (1995)","journal-title":"Formal Methods in System Design: An International Journal"},{"key":"26_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/3-540-45739-9_22","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"W. Damm","year":"2002","unstructured":"Damm, W., Jonsson, B.: Eliminating queues from rt uml models. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol.\u00a02469, p. 375. Springer, Heidelberg (2002)"},{"key":"26_CR11","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1023\/A:1008743212620","volume":"16","author":"J. Esparza","year":"2000","unstructured":"Esparza, J., Melzer, S.: Verification of safety properties using integer programming: Beyond the state equation. Formal Methods in System Design\u00a016, 159\u2013189 (2000)","journal-title":"Formal Methods in System Design"},{"issue":"3","key":"26_CR12","first-page":"143","volume":"30","author":"J. Esparza","year":"1994","unstructured":"Esparza, J., Nielsen, M.: Decibility issues for Petri nets - a survey. Journal of Informatik Processing and Cybernetics\u00a030(3), 143\u2013160 (1994)","journal-title":"Journal of Informatik Processing and Cybernetics"},{"key":"26_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/3-540-45314-8_8","volume-title":"Fundamental Approaches to Software Engineering","author":"C. Fischer","year":"2001","unstructured":"Fischer, C., Olderog, E.-R., Wehrheim, H.: A csp view on uml-rt structure diagrams. In: Hussmann, H. (ed.) FASE 2001. LNCS, vol.\u00a02029, p. 91. Springer, Heidelberg (2001)"},{"key":"26_CR14","doi-asserted-by":"crossref","unstructured":"Grosu, R., Broy, M., Selic, B., Stefanescu, G.: What is behind UML-RT? Behavioral specifications of businesses and systems (1999)","DOI":"10.1007\/978-1-4615-5229-1_6"},{"key":"26_CR15","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D. Harel","year":"1987","unstructured":"Harel, D.: Statecharts: A visual formalisation for complex systems. Science of Computer Programming\u00a08, 231\u2013274 (1987)","journal-title":"Science of Computer Programming"},{"key":"26_CR16","volume-title":"Proc. of the Fourth IEEE International Symposium on Object-Oriented Real-Time Distributed Computing ISORC 2001","author":"D. Herzberg","year":"2001","unstructured":"Herzberg, D., Marburger, A.: The use of layers and planes for architectural design of communication systems. In: Proc. of the Fourth IEEE International Symposium on Object-Oriented Real-Time Distributed Computing ISORC 2001, May 2001, IEEE Computer Society, Los Alamitos (2001)"},{"key":"26_CR17","volume-title":"The Spin Model Checker - Primer and Reference Manual","author":"G.J. Holzmann","year":"2004","unstructured":"Holzmann, G.J.: The Spin Model Checker - Primer and Reference Manual. Addison-Wesley, Reading (2004)"},{"key":"26_CR18","doi-asserted-by":"crossref","unstructured":"Jeron, T., Jard, C.: Testing for unboundedness of fifo channels. Theoretical Computer Science\u00a0(113), 93\u2013117 (1993)","DOI":"10.1016\/0304-3975(93)90212-C"},{"key":"26_CR19","unstructured":"Lipton, R.: The reachability problem requires exponential space. Technical Report 62, Department of Computer Science,Yale University (January 1976)"},{"key":"26_CR20","unstructured":"Lyons, A.: Developing and debugging real-time software with objectime developer (1999), available from http:\/\/www.objectime.com\/otl\/technical\/1999q1_p017.pdf"},{"issue":"1-3","key":"26_CR21","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1016\/S0304-3975(02)00646-1","volume":"297","author":"R. Mayr","year":"2003","unstructured":"Mayr, R.: Undecidable problems in unreliable computations. TCS\u00a0297(1-3), 337\u2013354 (2003)","journal-title":"TCS"},{"key":"26_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"250","DOI":"10.1007\/3-540-61055-3_41","volume-title":"Programming Languages and Systems - ESOP \u201996","author":"S. Melzer","year":"1996","unstructured":"Melzer, S., Esparza, J.: Checking system properties via integer programming. In: Riis Nielson, H. (ed.) ESOP 1996. LNCS, vol.\u00a01058, pp. 250\u2013264. Springer, Heidelberg (1996)"},{"key":"26_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/3-540-10001-6_24","volume-title":"Net Theory and Applications","author":"G. Memmi","year":"1980","unstructured":"Memmi, G., Roucairol, G.: Linear algebra in net theory. In: Brauer, W. (ed.) Net Theory and Applications. LNCS, vol.\u00a084, pp. 213\u2013223. Springer, Heidelberg (1980)"},{"key":"26_CR24","unstructured":"Saaltink, M.: Generating and analysing Promela from RoseRT models. Technical Report TR- 99-5537-02, ORA Canada, 1208 One Nocholas Street, Ottawa Ontario, K1N 7B7, Canada (1999)"},{"issue":"10","key":"26_CR25","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1145\/317665.317675","volume":"42","author":"B. Selic","year":"1999","unstructured":"Selic, B.: Turning clockwise: using UML in the real-time domain. Comm. of the ACM\u00a042(10), 46\u201354 (1999)","journal-title":"Comm. of the ACM"},{"key":"26_CR26","doi-asserted-by":"crossref","unstructured":"Selic, B.: An overview of uml 2.0. In: International Conference on Software Engineering, Tutorial Notes (May 2003)","DOI":"10.1109\/ICSE.2003.1201272"},{"key":"26_CR27","volume-title":"Real-Time Object-Oriented Modelling","author":"B. Selic","year":"1994","unstructured":"Selic, B., Gullekson, G., Ward, P.T.: Real-Time Object-Oriented Modelling. John Wiley & Sons, Inc., Chichester (1994)"},{"key":"26_CR28","doi-asserted-by":"crossref","unstructured":"Selic, B., Rumbaugh, J.: Using UML for modeling complex real-time systems (March 1998), http:\/\/www.rational.com\/media\/whitepapers\/umlrt.pdf","DOI":"10.1007\/BFb0057795"},{"issue":"1","key":"26_CR29","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/0890-5401(92)90059-O","volume":"96","author":"H. Yen","year":"1992","unstructured":"Yen, H.: A unified approach for deciding the existence of certain Petri net paths. Information and Computation\u00a096(1), 119\u2013137 (1992)","journal-title":"Information and Computation"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24730-2_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T03:18:27Z","timestamp":1559359107000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24730-2_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540212997","9783540247302"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24730-2_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}