{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,15]],"date-time":"2024-07-15T11:54:35Z","timestamp":1721044475522},"reference-count":41,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2003,6,17]],"date-time":"2003-06-17T00:00:00Z","timestamp":1055808000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2003,11]]},"DOI":"10.1007\/s10009-002-0094-1","type":"journal-article","created":{"date-parts":[[2004,3,20]],"date-time":"2004-03-20T15:40:18Z","timestamp":1079797218000},"page":"59-77","source":"Crossref","is-referenced-by-count":28,"title":["Automated test generation from timed automata"],"prefix":"10.1007","volume":"5","author":[{"given":"Brian","family":"Nielsen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Arne","family":"Skou","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,6,17]]},"reference":[{"key":"94_CR1","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"Alur","year":"2","unstructured":"Alur R, Dill DL: A theory of timed automata. Theoret Comput Sci 126(2):183\u2013235, 1994","journal-title":"Theoret Comput Sci"},{"key":"94_CR2","doi-asserted-by":"crossref","unstructured":"Alur R, Fix L, Henzinger TA: Event-clock automata: a determinizable class of timed automata. In: 6th Conference on Computer Aided Verification, Lecture Notes in Computer Science, vol. 818. Springer, Berlin Heidelberg New York, 1994","DOI":"10.1007\/3-540-58179-0_39"},{"key":"94_CR3","doi-asserted-by":"crossref","unstructured":"Behrmann G, Larsen KG, Pearson J, Weise C, Yi W: Efficient timed reachability analysis using clock difference diagrams. In: Computer Aided Verification (CAV\u201999), Lecture Notes in Computer Science, vol. 1633. Springer, Berlin Heidelberg New York, 1999, pp. 22\u201324","DOI":"10.1007\/3-540-48683-6_30"},{"key":"94_CR4","unstructured":"Beizer B: Software testing techniques. International Thompson Computer, New York, 1990"},{"key":"94_CR5","unstructured":"Bellman R: Dynamic programming. Princeton University Press, Princeton, New Jersey, 1957"},{"key":"94_CR6","doi-asserted-by":"crossref","unstructured":"Bengtsson J, David Griffioen WO, Kristoffersen KJ, Larsen KG, Larsson F, Petterson P, Yi W: Verification of an audio protocol with bus collision using UppAal. In: 9th Int. Conference on Computer Aided Verification, Lecture Notes in Computer Science, vol. 1102. Springer, Berlin Heidelberg New York, 1996, pp. 244\u2013256","DOI":"10.1007\/3-540-61474-5_73"},{"key":"94_CR7","doi-asserted-by":"crossref","unstructured":"Steffen B, Cleaveland R (eds.): Int J Software Tools Technol Transfer 1(1+2), 1997","DOI":"10.1007\/s100090050001"},{"key":"94_CR8","doi-asserted-by":"crossref","unstructured":"Bosscher D, Polak I, Vaandrager F: Verification of an audio protocol. TR CS-R9445, CWI, Amsterdam, The Netherlands, 1994; Lecture Notes in Computer Science, vol. 863. Springer, Berlin Heidelberg New York, 1994","DOI":"10.1007\/3-540-58468-4_165"},{"key":"94_CR9","unstructured":"Bouajjani A, Tripakis S, Yovine S: On-the-fly symbolic model-checking for real-time systems. In: 1997 IEEE Real-Time Systems Symposium, RTSS\u201997, San Fransisco, Calif., USA. IEEE Computer, New York, 1996"},{"key":"94_CR10","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/S0167-6423(99)00017-9","volume":"36","author":"Bozga","year":"1","unstructured":"Bozga M, Fernandez JC, Ghirvu L, Jard C, J\u00e9ron T, Kerbrat A, Morel P, Mounier L: Verification and test generation for the SSCOP protocol. Sci Comput Program 36(1):27\u201352, 2000","journal-title":"Sci Comput Program"},{"key":"94_CR11","doi-asserted-by":"crossref","unstructured":"Bozga M, Fernandez JC, Kerbrat A, Mounier L: Protocol verification with the ALD\u00c9BARAN toolset. Int J Software Tools Technol Transfer 1(1+2):166\u2013184, 1997","DOI":"10.1007\/s100090050012"},{"key":"94_CR12","unstructured":"Braberman V, Felder M, Marr\u00e9 M: Testing timing behaviors of real time software. In: Quality Week 1997. San Francisco, Calif., USA, 1997, pp. 143\u2013155"},{"key":"94_CR13","unstructured":"Brinksma E: A theory for the derivation of tests. In: Protocol Specification Testing and Verification VIII (PSTV\u201988), 1988, pp. 63\u201374"},{"key":"94_CR14","doi-asserted-by":"crossref","first-page":"350","DOI":"10.1007\/s001650070009","volume":"12","author":"Cardell-Oliver","year":"5","unstructured":"Cardell-Oliver R: Conformance testing of real-time systems with timed automata. Formal Aspects Comput 12(5):350\u2013371, 2000","journal-title":"Formal Aspects Comput"},{"key":"94_CR15","doi-asserted-by":"crossref","unstructured":"Cardell-Oliver R, Glover T: A practical and complete algorithm for testing real-time systems. In: 5th international Symposium on Formal Techniques in Real Time and Fault Tolerant Systems (FTRTFT\u201998), September 14\u201318, Lecture Notes in Computer Science, vol. 1486. Springer, Berlin Heidelberg New York, 1998, pp. 251\u2013261","DOI":"10.1007\/BFb0055352"},{"key":"94_CR16","doi-asserted-by":"crossref","unstructured":"Castanet R, Kon\u00e9 O, Lauren\u00e7ot P: On-the-fly test generation for real-time protocols. In: International Conference in Computer Communications and Networks, Lafayette, La., USA, October 12\u201315. IEEE Computer, New York, 1998","DOI":"10.1109\/ICCCN.1998.998798"},{"key":"94_CR17","doi-asserted-by":"crossref","unstructured":"Clarke D, Lee I: Testing real-time constraints in a process algebraic setting. In: 17th International Conference on Software Engineering, 1995","DOI":"10.1145\/225014.225019"},{"key":"94_CR18","doi-asserted-by":"crossref","unstructured":"Clarke D, Lee I: Automatic test generation for the analysis of a real-time system: case study. In: 3rd IEEE Real-Time Technology and Applications Symposium, 1997","DOI":"10.1109\/RTTAS.1997.601349"},{"key":"94_CR19","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF01211314","volume":"5","author":"Cleaveland","year":"1993","unstructured":"Cleaveland R, Hennessy M: Testing equivalence as a bisimulation equivalence. Formal Aspects Comput 5:1\u201320, 1993","journal-title":"Formal Aspects Comput"},{"key":"94_CR20","doi-asserted-by":"crossref","unstructured":"Daws C, Yovine S: Reducing the number of clock variables of timed automata. In: 1996 IEEE Real-Time Systems Symposium, RTSS\u201996, Washington, DC, USA. IEEE Computer, New York, 1996","DOI":"10.1109\/REAL.1996.563702"},{"key":"94_CR21","first-page":"382","volume":"2","author":"de","year":"4","unstructured":"de Vries RG, Tretmans J: On-the-fly conformance testing using SPIN. Int Jn Software Tools Technol Transfer 2(4):382\u2013393, 2000","journal-title":"Int Jn Software Tools Technol Transfer"},{"key":"94_CR22","doi-asserted-by":"crossref","unstructured":"Dill DL: Timing assumptions and verification of finite-state concurrent systems. In: International Workshop on Automatic Verification Methods for Finite State Systems, Grenoble, France, June. Lecture Notes in Computer Science, vol. 407. Springer, Berlin Heidelberg New York, 1989, pp. 197\u2013212","DOI":"10.1007\/3-540-52148-8_17"},{"key":"94_CR23","doi-asserted-by":"crossref","unstructured":"En-Nouaary A, Dssouli R, Khendek F: Timed test cases generation based on state characterization technique. In: 19th IEEE Real-Time Systems Symposium (RTSS\u201998), 1998, pp. 220\u2013229","DOI":"10.1109\/REAL.1998.739748"},{"key":"94_CR24","unstructured":"Holzmann JG: Design and validation of computer protocols. Prentice-Hall, N.J., USA, 1991"},{"key":"94_CR25","doi-asserted-by":"crossref","unstructured":"Kerbrat A, J\u00e9ron T, Groz R: Automated test generation from SDL specifications. In: 9th SDL Forum, 21\u201325 June. Montr\u00e9al, Qu\u00e9bec, Canada, 1999","DOI":"10.1016\/B978-044450228-5\/50011-4"},{"key":"94_CR26","unstructured":"Koustsofios E, North SC: Drawing graphs with dot. Technical Report http:\/\/www.research.att.com\/sw\/tools\/graphviz\/ dotguide.ps.gz, AT&T Bell Laboratories, Murray Hill, N.J., USA, 1999"},{"key":"94_CR27","doi-asserted-by":"crossref","unstructured":"Larsen KG, Larsson F, Petterson P, Yi W: Efficient verification of real-time systems: compact data structures and state-space reduction. In: 18th IEEE Real-Time Systems Symposium, 1997, pp. 14\u201324","DOI":"10.1109\/REAL.1997.641265"},{"key":"94_CR28","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"Larsen","year":"1","unstructured":"Larsen KG, Pettersson P, Yi W: UppAal in a nutshell. Int J Software Tools Technol Transfer 1(1):134\u2013152, 1997","journal-title":"Int J Software Tools Technol Transfer"},{"key":"94_CR29","doi-asserted-by":"crossref","unstructured":"Leblanc P: OMT and SDL based techniques and tools for design, simulation and test production of distributed systems. Int J Software Tools Technol Transfer 1(1+2):153\u2013165, 1997","DOI":"10.1007\/s100090050011"},{"key":"94_CR30","doi-asserted-by":"crossref","first-page":"365","DOI":"10.1145\/210223.210226","volume":"13","author":"Mandrioli","year":"1995","unstructured":"Mandrioli D, Morasca S, Morzenti A: Generating test cases for real-time systems from logic specifications. ACM Trans Comput Syst 13(4):365\u2013398, 1995","journal-title":"ACM Trans Comput Syst"},{"key":"94_CR31","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1016\/0304-3975(84)90113-0","volume":"34","author":"De","year":"1984","unstructured":"De Nicola R, Hennessy MCB: Testing equivalences for processes. Theoret Comput Sci 34:83\u2013133, 1984","journal-title":"Theoret Comput Sci"},{"key":"94_CR32","unstructured":"Nielsen B: Specification and test of real-time systems. PhD thesis, Department of Computer Science, Aalborg University, Denmark, 2000"},{"key":"94_CR33","doi-asserted-by":"crossref","unstructured":"Peleska J, Buth B: Formal methods for the international space station ISS. In: Olderog ER, Steffen B (eds) Correct System Design. Lecture Notes in Computer Science, vol. 1710. Springer, Berlin Heidelberg New York, 1999, pp. 363\u2013389","DOI":"10.1007\/3-540-48092-7_16"},{"key":"94_CR34","unstructured":"Peleska J, Zahlten C: Test automation for avionic systems and space technology. In: GI Working Group on Test, Analysis and Verification of Software. Munich (extended abstract), 1999"},{"key":"94_CR35","unstructured":"Ressouche A, de Simone R, Bouali A, Roy V. The fcTools user manual. Technical Report ftp:\/\/ftp-sop.inria.fr\/meije\/verif\/fc2.userman.ps, INRIA Sophia Antipolis"},{"key":"94_CR36","unstructured":"Rushby J: Formal methods: instruments of justification or tools of discovery. In: Nordic Seminar on Dependable Computing Systems (NSDCS\u201994), Lyngby, Denmark, 1994"},{"key":"94_CR37","unstructured":"Schlingloff H, Meyer O, H\u00fclsing T: Correctness analysis of an embedded controller. In: Data Systems in Aerospace (DASIA99). ESA SP-447, Lisbon, Portugal, 1999, pp. 317\u2013325"},{"key":"94_CR38","doi-asserted-by":"crossref","unstructured":"Schmitt M, Koch B, Grabowski J, Hogrefe D: Autolink \u2013 Putting formal test methods into practice. In: 11th Int. Workshop on Testing of Communicating Systems (IWTCS\u201998), Tomsk, Russia, 1998","DOI":"10.1007\/978-0-387-35381-4_14"},{"key":"94_CR39","doi-asserted-by":"crossref","unstructured":"Springintveld J, Vaandrager F, D\u2019Argenio PR: Testing timed automata. TR CTIT 97-17, University of Twente. Theoret Comput Sci 254(1\u20132):225\u2013257, 2001","DOI":"10.1016\/S0304-3975(99)00134-6"},{"key":"94_CR40","doi-asserted-by":"crossref","unstructured":"Diekert V, Gastin P, Petit A: Removing epsilon-transitions in timed automata. In: 14th Annual Symposium on Theoretical Aspects of Computer Science, STACS 1997, L\u00fcbeck, Germany, February 27 \u2013 March 1 1997. Lecture Notes in Computer Science, vol. 1200. Springer, Berlin Heidelberg New York, 1997, pp. 583\u2013594","DOI":"10.1007\/BFb0023491"},{"key":"94_CR41","unstructured":"Yi W, Pettersson P, Daniels M: Automatic verification of real-time communicating systems by constraint solving. In: 7th Int. Conf. on Formal Description Techniques. North-Holland, Amsterdam, The Netherlands, 1994, pp. 223\u2013238"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-002-0094-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-002-0094-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-002-0094-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,31]],"date-time":"2020-03-31T18:11:35Z","timestamp":1585678295000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-002-0094-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,6,17]]},"references-count":41,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2003,11]]}},"alternative-id":["94"],"URL":"https:\/\/doi.org\/10.1007\/s10009-002-0094-1","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2003,6,17]]}}}