{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T09:57:28Z","timestamp":1773655048156,"version":"3.50.1"},"reference-count":35,"publisher":"Elsevier BV","issue":"1-2","license":[{"start":{"date-parts":[[2001,3,1]],"date-time":"2001-03-01T00:00:00Z","timestamp":983404800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":4521,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[2001,3]]},"DOI":"10.1016\/s0304-3975(99)00134-6","type":"journal-article","created":{"date-parts":[[2002,7,25]],"date-time":"2002-07-25T20:01:16Z","timestamp":1027627276000},"page":"225-257","source":"Crossref","is-referenced-by-count":183,"title":["Testing timed automata"],"prefix":"10.1016","volume":"254","author":[{"given":"Jan","family":"Springintveld","sequence":"first","affiliation":[]},{"given":"Frits","family":"Vaandrager","sequence":"additional","affiliation":[]},{"given":"Pedro","family":"R. D'Argenio","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"issue":"11","key":"10.1016\/S0304-3975(99)00134-6_BIB1","doi-asserted-by":"crossref","first-page":"1604","DOI":"10.1109\/26.111442","article-title":"An optimization technique for protocol conformance test generation based on UIO sequences and Rural Chinese Postman Tours","volume":"39","author":"Aho","year":"1991","journal-title":"IEEE Trans. Comm."},{"key":"10.1016\/S0304-3975(99)00134-6_BIB2","doi-asserted-by":"crossref","unstructured":"R. Alur, D.L. Dill, A theory of timed automata, Theoret. Comput. Sci. 126 (1994) 183\u2013235. Preliminary versions of this paper appear in the Proc. 17th Internat. Colloq. on Automata, Languages, and Programming (1990), and in the Proc. REX workshop \u201cReal-Time: Theory in Practice\u201d (1991).","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"10.1016\/S0304-3975(99)00134-6_BIB3","doi-asserted-by":"crossref","unstructured":"R. Alur, T.A. Henzinger (Eds.), Proc. 8th Internat. Conf. Computer Aided Verification, New Brunswick, NJ, USA, Lecture Notes in Computer Science, Vol. 1102, Springer, Berlin, July\/August 1996.","DOI":"10.1007\/3-540-61474-5"},{"key":"10.1016\/S0304-3975(99)00134-6_BIB4","doi-asserted-by":"crossref","unstructured":"R. Alur, T.A. Henzinger, E.D. Sontag (Eds.), Hybrid Systems III, Lecture Notes in Computer Science, Vol. 1066, Springer, Berlin, 1996.","DOI":"10.1007\/BFb0020948"},{"key":"10.1016\/S0304-3975(99)00134-6_BIB5","first-page":"220","article-title":"Timing analysis in COSPAN","volume":"Vol. 1066","author":"Alur","year":"1996"},{"key":"10.1016\/S0304-3975(99)00134-6_BIB6","doi-asserted-by":"crossref","unstructured":"J. Bengtsson, W.O.D. Griffioen, K.J. Kristoffersen, K.G. Larsen, F. Larsson, P. Pettersson, Wang Yi, Verification of an audio protocol with bus collision using UPPAAL, in: Alur, Henzinger (Eds.), Proc. 8th Internat. Conf. Computer Aided Verification, New Brunswick, NJ, USA, Lecture Notes in Computer Science, Vol. 1102, Springer, Berlin, July\/August 1996, pp. 244\u2013256.","DOI":"10.1007\/3-540-61474-5_73"},{"key":"10.1016\/S0304-3975(99)00134-6_BIB7","first-page":"251","article-title":"A practical and complete algorithm for testing real-time systems","volume":"Vol. 1486","author":"Cardell-Oliver","year":"1998"},{"key":"10.1016\/S0304-3975(99)00134-6_BIB8","unstructured":"K. C\u0306er\u0101ns, Algorithmic problems in analysis of real time system specifications, Dr.sc.comp. Thesis, University of Latvia, R\u0131\u0304ga, 1992."},{"key":"10.1016\/S0304-3975(99)00134-6_BIB9","first-page":"302","article-title":"Decidability of bisimulation equivalences for parallel timer processes","volume":"Vol. 663","author":"C\u0306er\u0101ns","year":"1992"},{"key":"10.1016\/S0304-3975(99)00134-6_BIB10","doi-asserted-by":"crossref","unstructured":"W.Y.L. Chan, S.T. Vuong, M.R. Ito, An improved protocol test generation procedure based on UIOs, in Proc. ACM Symp. on Communication Architectures and Protocols, ACM, 1989, pp. 283\u2013294.","DOI":"10.1145\/75246.75274"},{"issue":"3","key":"10.1016\/S0304-3975(99)00134-6_BIB11","doi-asserted-by":"crossref","first-page":"178","DOI":"10.1109\/TSE.1978.231496","article-title":"Testing software design modeled by finite-state machines","volume":"4","author":"Chow","year":"1978","journal-title":"IEEE Trans. Software Eng."},{"key":"10.1016\/S0304-3975(99)00134-6_BIB12","doi-asserted-by":"crossref","unstructured":"D. Clarke, I. Lee, Automatic generation of tests for timing constraints from requirements, in Proc. 3rd Internat. Workshop on Object Oriented Real-Time Dependable Systems, Newport Beach, California, February 1997.","DOI":"10.1109\/WORDS.1997.609955"},{"key":"10.1016\/S0304-3975(99)00134-6_BIB13","doi-asserted-by":"crossref","unstructured":"P.R. D'Argenio, J.-P. Katoen, T.C. Ruys, J. Tretmans, The bounded retransmission protocol must be on time! in: E. Brinksma (Ed.), Proc. 3rd Workshop on Tools and Algorithms for the Construction and Analysis of Systems, Enschede, The Netherlands, Lecture Notes in Computer Science, Vol. 1217, Springer, Berlin, April 1997, pp. 416\u2013431.","DOI":"10.1007\/BFb0035403"},{"key":"10.1016\/S0304-3975(99)00134-6_BIB14","first-page":"208","article-title":"The tool KRONOS","volume":"Vol. 1066","author":"Daws","year":"1996"},{"key":"10.1016\/S0304-3975(99)00134-6_BIB15","doi-asserted-by":"crossref","unstructured":"C. Daws, S. Yovine, Two examples of verification of multirate timed automata with KRONOS, in Proc. 16th IEEE Real-Time Systems Symp. (RTSS\u201995), Pisa, Italy, IEEE Computer Society Press, Silver Spring, MD, December 1995, pp. 66\u201375.","DOI":"10.1109\/REAL.1995.495197"},{"key":"10.1016\/S0304-3975(99)00134-6_BIB16","doi-asserted-by":"crossref","unstructured":"A. En-Nouaary, R. Dssouli, F. Khendek, A. Elqortobi, Timed test cases generation based on state characterization technique, in Proc. 19th IEEE Real-Time Systems Symposium (RTSS\u201998), Madrid, Spain. IEEE Computer Society Press, Silver Spring, MD, December 1998, pp. 220\u2013229.","DOI":"10.1109\/REAL.1998.739748"},{"key":"10.1016\/S0304-3975(99)00134-6_BIB17","doi-asserted-by":"crossref","unstructured":"J.-C. Fernandez, C. Jard, Th. J\u00e9ron, C. Viho, Using on-the-fly verification techniques for the generation of test suites, in: Alur, Henzinger (Eds.), Proc. 8th Internat. Conf. Computer Aided Verification, New Brunswick, NJ, USA, Lecture Notes in Computer Science, Vol. 1102, Springer, Berlin, July\/August 1996, pp. 348\u2013359.","DOI":"10.1007\/3-540-61474-5_82"},{"key":"10.1016\/S0304-3975(99)00134-6_BIB18","first-page":"331","article-title":"Robust timed automata","volume":"Vol. 1201","author":"Gupta","year":"1997"},{"key":"10.1016\/S0304-3975(99)00134-6_BIB19","doi-asserted-by":"crossref","unstructured":"T.A. Henzinger, P.-H. Ho, HyTech: the Cornell HYbrid TECHnology tool, in: U.H. Engberg, K.G. Larsen, A. Skou (Eds.), Proc. Workshop on Tools and Algorithms for the Construction and Analysis of Systems, Aarhus, Denmark, BRICS Notes Series, Vol. NS-95-2, Department of Computer Science, University of Aarhus, May 1995, pp. 29\u201343.","DOI":"10.1007\/3-540-60472-3_14"},{"key":"10.1016\/S0304-3975(99)00134-6_BIB20","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1006\/inco.1994.1045","article-title":"Symbolic model checking for real-time systems","volume":"111","author":"Henzinger","year":"1994","journal-title":"Inform. Comput."},{"key":"10.1016\/S0304-3975(99)00134-6_BIB21","doi-asserted-by":"crossref","unstructured":"P.-H. Ho, H. Wong-Toi, Automated analysis of an audio control protocol, in: P. Wolper (Ed.), Proc. 7th Internat. Conf. on Computer Aided Verification, Li\u00e8ge, Belgium, Lecture Notes in Computer Science, Vol. 939, Springer, Berlin, June 1995, pp. 381\u2013394.","DOI":"10.1007\/3-540-60045-0_64"},{"key":"10.1016\/S0304-3975(99)00134-6_BIB22","series-title":"Design and Validation of Computer Protocols","author":"Holzmann","year":"1991"},{"key":"10.1016\/S0304-3975(99)00134-6_BIB23","series-title":"Switching and Finite Automata Theory","author":"Kohavi","year":"1978"},{"issue":"1\/2","key":"10.1016\/S0304-3975(99)00134-6_BIB24","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/s100090050010","article-title":"UPPAAL in a nutshell","volume":"1","author":"Larsen","year":"1997","journal-title":"Internat. J. Software Tools Technol. Transfer"},{"key":"10.1016\/S0304-3975(99)00134-6_BIB25","doi-asserted-by":"crossref","unstructured":"N.A. Lynch, M.R. Tuttle, Hierarchical correctness proofs for distributed algorithms, in Proc. 6th Annual ACM Symp. on Principles of Distributed Computing, August 1987, pp. 137\u2013151. A full version is available as MIT Technical Report MIT\/LCS\/TR-387.","DOI":"10.1145\/41840.41852"},{"issue":"4","key":"10.1016\/S0304-3975(99)00134-6_BIB26","doi-asserted-by":"crossref","first-page":"365","DOI":"10.1145\/210223.210226","article-title":"Generating test cases for real-time systems from logic specifications","volume":"13","author":"Mandrioli","year":"1995","journal-title":"ACM Trans. Comput. Systems"},{"key":"10.1016\/S0304-3975(99)00134-6_BIB27","unstructured":"A. Petrenko, T. Higashino, T. Kaji, Handling redundant and additional states in protocol testing, in: A. Cavalli, S. Budkowski (Eds.), Proc. 8th Internat. Workshop on Protocol Test Systems IWPTS \u201995, Paris, France, 1995, pp. 307\u2013322."},{"key":"10.1016\/S0304-3975(99)00134-6_BIB28","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1006\/inco.1997.2671","article-title":"Liveness in timed and untimed systems","volume":"141","author":"Segala","year":"1998","journal-title":"Inform. Comput."},{"key":"10.1016\/S0304-3975(99)00134-6_BIB29","series-title":"Software Engineering","author":"Sommerville","year":"1996"},{"key":"10.1016\/S0304-3975(99)00134-6_BIB30","first-page":"130","article-title":"Minimizable timed automata","volume":"Vol. 1135","author":"Springintveld","year":"1996"},{"key":"10.1016\/S0304-3975(99)00134-6_BIB31","unstructured":"J. Tretmans, A formal approach to conformance testing, Ph.D. Thesis, University of Twente, December 1992."},{"key":"10.1016\/S0304-3975(99)00134-6_BIB32","doi-asserted-by":"crossref","unstructured":"J. Tretmans, Test generation with inputs, outputs, and quiescence, in: T. Margaria, B. Steffen (Eds.), Proc. 2nd. Workshop on Tools and Algorithms for the Construction and Analysis of Systems, Passau, Germany, Lecture Notes in Computer Science, Vol. 1055, Springer, Berlin, April 1996, pp. 127\u2013146.","DOI":"10.1007\/3-540-61042-1_42"},{"key":"10.1016\/S0304-3975(99)00134-6_BIB33","first-page":"103","article-title":"Test generation with inputs, outputs, and repetitive quiescence","volume":"17","author":"Tretmans","year":"1996","journal-title":"Software \u2014 Concepts and Tools"},{"key":"10.1016\/S0304-3975(99)00134-6_BIB34","doi-asserted-by":"crossref","unstructured":"C. Weise, D. Lenzkes, Efficient scaling-invariant checking of timed bisimulation, in: R. Reischuk, M. Morvan (Eds.), Proc. 14th Symp. on Theoretical Aspects of Computer Science STACS \u201997, L\u00fcbeck, Germany, Lecture Notes in Computer Science, Vol. 1200, Springer, Berlin, February 1997, pp. 177\u2013188.","DOI":"10.1007\/BFb0023458"},{"key":"10.1016\/S0304-3975(99)00134-6_BIB35","first-page":"502","article-title":"Real-time behaviour of asynchronous agents","volume":"Vol. 458","author":"Yi","year":"1990"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397599001346?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397599001346?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,22]],"date-time":"2019-04-22T00:59:56Z","timestamp":1555894796000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397599001346"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,3]]},"references-count":35,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2001,3]]}},"alternative-id":["S0304397599001346"],"URL":"https:\/\/doi.org\/10.1016\/s0304-3975(99)00134-6","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[2001,3]]}}}