{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,12]],"date-time":"2026-03-12T14:04:42Z","timestamp":1773324282681,"version":"3.50.1"},"reference-count":50,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2009,2,14]],"date-time":"2009-02-14T00:00:00Z","timestamp":1234569600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2009,6]]},"DOI":"10.1007\/s10703-009-0065-1","type":"journal-article","created":{"date-parts":[[2009,2,16]],"date-time":"2009-02-16T09:39:15Z","timestamp":1234777155000},"page":"238-304","source":"Crossref","is-referenced-by-count":123,"title":["Conformance testing for real-time systems"],"prefix":"10.1007","volume":"34","author":[{"given":"Moez","family":"Krichen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stavros","family":"Tripakis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2009,2,14]]},"reference":[{"key":"65_CR1","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur R, Dill D (1994) A theory of timed automata. Theor Comput Sci 126:183\u2013235","journal-title":"Theor Comput Sci"},{"key":"65_CR2","series-title":"LNCS","volume-title":"CAV\u201994","author":"R Alur","year":"1994","unstructured":"Alur R, Fix L, Henzinger T (1994) A determinizable class of timed automata. In: CAV\u201994. LNCS, vol\u00a0818. Springer, Berlin"},{"key":"65_CR3","volume-title":"12th international workshop on testing of communicating systems","author":"A Belinfante","year":"1999","unstructured":"Belinfante A, Feenstra J, de Vries RG, Tretmans J, Goga N, Feijs L, Mauw S, Heerink L (1999) Formal test automation: a simple experiment. In: 12th international workshop on testing of communicating systems. Kluwer, Dordrecht"},{"key":"65_CR4","series-title":"LNCS","volume-title":"ICFEM\u201903","author":"J Bengtsson","year":"2003","unstructured":"Bengtsson J, Yi W (2003) On clock difference constraints and termination in reachability analysis of timed automata. In: ICFEM\u201903. LNCS, vol 2885. Springer, Berlin"},{"key":"65_CR5","series-title":"ENTCS","first-page":"23","volume-title":"4th international workshop on runtime verification (RV\u201904)","author":"S Bensalem","year":"2005","unstructured":"Bensalem S, Bozga M, Krichen M, Tripakis S (2005) Testing conformance of real-time applications by automatic generation of observers. In: 4th international workshop on runtime verification (RV\u201904). ENTCS, vol 113. Elsevier, Amsterdam, pp 23\u201343"},{"issue":"2\u20133","key":"65_CR6","doi-asserted-by":"crossref","first-page":"145","DOI":"10.3233\/FI-1998-36233","volume":"36","author":"B Berard","year":"1998","unstructured":"Berard B, Petit A, Diekert V, Gastin P (1998) Characterization of the expressive power of silent transitions in timed automata. Fund Inform 36(2\u20133):145\u2013182","journal-title":"Fund Inform"},{"key":"65_CR7","first-page":"41","volume":"9","author":"B Berthomieu","year":"1983","unstructured":"Berthomieu B, Menasche M (1983) An enumerative approach for analyzing time Petri nets. IFIP Congr Ser 9:41\u201346","journal-title":"IFIP Congr Ser"},{"key":"65_CR8","unstructured":"Blom J, Hessel A, Jonsson B, Pettersson P (2004) Specifying and generating test cases using observer automata. In: Proceedings of formal approaches to software testing, pp 125\u2013139"},{"key":"65_CR9","series-title":"LNCS","volume-title":"Compositionality","author":"S Bornot","year":"1998","unstructured":"Bornot S, Sifakis J, Tripakis S (1998) Modeling urgency in timed systems. In: Compositionality. LNCS, vol 1536. Springer, Berlin"},{"issue":"3","key":"65_CR10","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1023\/B:FORM.0000026093.21513.31","volume":"24","author":"P Bouyer","year":"2004","unstructured":"Bouyer P (2004) Forward analysis of updatable timed automata. Formal Methods in System Design 24(3):281\u2013320","journal-title":"Formal Methods in System Design"},{"key":"65_CR11","series-title":"LNCS","first-page":"219","volume-title":"FoSSaCS\u201905","author":"P Bouyer","year":"2005","unstructured":"Bouyer P, Chevalier F, D\u2019Souza D (2005) Fault diagnosis using timed automata. In: FoSSaCS\u201905. LNCS, vol 3441. Springer, Berlin, pp 219\u2013233"},{"key":"65_CR12","series-title":"LNCS","volume-title":"Proc CAV\u201900","author":"M Bozga","year":"2000","unstructured":"Bozga M, Fernandez JC, Ghirvu L, Graf S, Krimm JP, Mounier L (2000) IF: a validation environment for timed asynchronous systems. In: Proc CAV\u201900. LNCS, vol 1855. Springer, Berlin"},{"key":"65_CR13","unstructured":"Bozga M, Graf S, Kerbrat A, Mounier L, Ober I, Vincent D (2000) SDL for real-time: what is missing? In: Proceedings of SAM\u201900: 2nd workshop on SDL and MSC, Grenoble, France, pp\u00a0108\u2013122. IMAG, June 2000"},{"key":"65_CR14","unstructured":"Braberman V, Felder M, Marre M (1997) Testing timing behavior of real-time software. In: International software quality week"},{"key":"65_CR15","doi-asserted-by":"crossref","unstructured":"Brat G, Giannakopoulou D, Goldberg A, Havelund K, Lowry M, Pasareanu C, Venet A, Visser W (2003) Experimental evaluation of V&V tools on martian rover software. In: SEI software model checking workshop","DOI":"10.1023\/B:FORM.0000040027.28662.a4"},{"key":"65_CR16","series-title":"LNCS","volume-title":"MOVEP 2000","author":"E Brinksma","year":"2001","unstructured":"Brinksma E, Tretmans J (2001) Testing transition systems: an annotated bibliography. In: MOVEP 2000. LNCS, vol 2067. Springer, Berlin"},{"key":"65_CR17","series-title":"LNCS","volume-title":"FATES\u201904","author":"L Briones","year":"2004","unstructured":"Briones L, Brinksma E (2004) A test generation framework for quiescent real-time systems. In: FATES\u201904. LNCS, vol 3395. Springer, Berlin"},{"key":"65_CR18","volume-title":"ISSTA\u201902","author":"R Cardell-Oliver","year":"2002","unstructured":"Cardell-Oliver R (2002) Conformance test experiments for distributed real-time systems. In: ISSTA\u201902. ACM, New York"},{"key":"65_CR19","doi-asserted-by":"crossref","unstructured":"Chow TS (1978) Testing software design modeled by finite-state machines. IEEE Trans Softw Eng 4(1)","DOI":"10.1109\/TSE.1978.231496"},{"key":"65_CR20","series-title":"LNCS","volume-title":"TACAS\u201902","author":"D Clarke","year":"2002","unstructured":"Clarke D, J\u00e9ron T, Rusu V, Zinovieva E (2002) STG: a symbolic test generation tool. In: TACAS\u201902. LNCS, vol 2280. Springer, Berlin"},{"key":"65_CR21","doi-asserted-by":"crossref","unstructured":"Clarke D, Lee I (1997) Automatic generation of tests for timing constraints from requirements. In: 3rd workshop on object-oriented real-time dependable systems (WORDS\u201997)","DOI":"10.1109\/WORDS.1997.609955"},{"key":"65_CR22","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"208","DOI":"10.1007\/BFb0020947","volume-title":"Hybrid systems III, verification and control","author":"C Daws","year":"1996","unstructured":"Daws C, Olivero A, Tripakis S, Yovine S (1996) The tool Kronos. In: Hybrid systems III, verification and control. LNCS, vol 1066. Springer, Berlin, pp 208\u2013219"},{"key":"65_CR23","series-title":"LNCS","volume-title":"Tools and algorithms for the construction and analysis of systems \u201998, Lisbon, Portugal","author":"C Daws","year":"1998","unstructured":"Daws C, Tripakis S (1998) Model checking of real-time reachability properties using abstractions. In: Tools and algorithms for the construction and analysis of systems \u201998, Lisbon, Portugal. LNCS, vol 1384. Springer, Berlin"},{"key":"65_CR24","series-title":"LNCS","first-page":"197","volume-title":"Automatic verification methods for finite state systems","author":"D Dill","year":"1989","unstructured":"Dill D (1989) Timing assumptions and verification of finite-state concurrent systems. In: Sifakis J (ed) Automatic verification methods for finite state systems. LNCS, vol 407. Springer, Berlin, pp 197\u2013212"},{"key":"65_CR25","volume-title":"RTSS\u201998","author":"A En-Nouaary","year":"1998","unstructured":"En-Nouaary A, Dssouli R, Khendek F, Elqortobi A (1998) Timed test cases generation based on state characterization technique. In: RTSS\u201998. IEEE, New York"},{"key":"65_CR26","series-title":"LNCS","volume-title":"CAV\u201996","author":"JC Fernandez","year":"1996","unstructured":"Fernandez JC, Jard C, J\u00e9ron T, Viho G (1996) Using on-the-fly verification techniques for the generation of test suites. In: CAV\u201996. LNCS, vol 1102. Springer, Berlin"},{"key":"65_CR27","doi-asserted-by":"crossref","unstructured":"Groote JF, van de Pol J (1996) A bounded retransmission protocol for large data packets. In: Algebraic methodology and software technology, pp 536\u2013550","DOI":"10.1007\/BFb0014338"},{"key":"65_CR28","series-title":"LNCS","volume-title":"ICALP\u201992","author":"T Henzinger","year":"1992","unstructured":"Henzinger T, Manna Z, Pnueli A (1992) What good are digital clocks? In: ICALP\u201992. LNCS, vol 623. Springer, Berlin"},{"key":"65_CR29","unstructured":"Hessel A, Larsen K, Nielsen B, Pettersson P, Skou A (2003) Time-optimal real-time test case generation using UPPAAL. In: FATES\u201903"},{"key":"65_CR30","volume-title":"IFIP international workshop on testing of Communicating Systems","author":"T Higashino","year":"1999","unstructured":"Higashino T, Nakata A, Taniguchi K, Cavalli A (1999) Generating test cases for a timed I\/O automaton model. In: IFIP international workshop on testing of Communicating Systems. Kluwer, Dordrecht"},{"key":"65_CR31","unstructured":"ISO\/IEC (1992) Open systems interconnection conformance testing methodology and framework\u2014part 1: general concept; part 2: abstract test suite specification; part 3: the tree and tabular combined notation (TTCN). Technical Report 9646, International Organization for Standardization\u2014Information Processing Systems\u2014Open Systems Interconnection, Gen\u00e8ve"},{"key":"65_CR32","doi-asserted-by":"crossref","unstructured":"Jard C, J\u00e9ron T, Morel P (2000) Verification of test suites. In: TestCom 2000","DOI":"10.1007\/978-0-387-35516-0_1"},{"key":"65_CR33","unstructured":"Khoumsi A, J\u00e9ron T, Marchand H (2003) Test cases generation for nondeterministic real-time systems. In: FATES\u201903"},{"key":"65_CR34","series-title":"LNCS","volume-title":"11th international spin workshop on model checking of software (SPIN\u201904)","author":"M Krichen","year":"2004","unstructured":"Krichen M, Tripakis S (2004) Black-box conformance testing for real-time systems. In: 11th international spin workshop on model checking of software (SPIN\u201904). LNCS, vol 2989. Springer, Berlin"},{"key":"65_CR35","series-title":"LNCS","volume-title":"Formal techniques, modelling and analysis of timed and fault tolerant systems (FORMATS-FTRTFT\u201904)","author":"M Krichen","year":"2004","unstructured":"Krichen M, Tripakis S (2004) Real-time testing with timed automata testers and coverage criteria. In: Formal techniques, modelling and analysis of timed and fault tolerant systems (FORMATS-FTRTFT\u201904). LNCS, vol 3253. Springer, Berlin"},{"key":"65_CR36","series-title":"LNCS","volume-title":"The 17th IFIP international conference on testing of communicating systems (TestCom\u201905)","author":"M Krichen","year":"2005","unstructured":"Krichen M, Tripakis S (2005) An expressive and implementable formal framework for testing real-time systems. In: The 17th IFIP international conference on testing of communicating systems (TestCom\u201905). LNCS, vol 3502. Springer, Berlin"},{"key":"65_CR37","series-title":"LNCS","volume-title":"The 17th IFIP international conference on testing of communicating systems (TestCom\u201905)","author":"M Krichen","year":"2005","unstructured":"Krichen M, Tripakis S (2005) State identification problems for timed automata. In: The 17th IFIP international conference on testing of communicating systems (TestCom\u201905). LNCS, vol 3502. Springer, Berlin"},{"key":"65_CR38","series-title":"LNCS","volume-title":"FATES\u201904","author":"K Larsen","year":"2004","unstructured":"Larsen K, Mikucionis M, Nielsen B (2004) Online testing of real-time systems using uppaal. In: FATES\u201904. LNCS, vol 3395. Springer, Berlin"},{"key":"65_CR39","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1145\/1086228.1086283","volume-title":"5th ACM international conference on embedded software","author":"K Larsen","year":"2005","unstructured":"Larsen K, Mikucionis M, Nielsen B, Skou A (2005) Testing real-time embedded software using UPPAAL-TRON: an industrial case study. In: 5th ACM international conference on embedded software. ACM, New York, pp 299\u2013306"},{"key":"65_CR40","doi-asserted-by":"crossref","first-page":"1090","DOI":"10.1109\/5.533956","volume":"84","author":"D Lee","year":"1996","unstructured":"Lee D, Yannakakis M (1996) Principles and methods of testing finite state machines\u2014a survey. Proc IEEE 84:1090\u20131126","journal-title":"Proc IEEE"},{"key":"65_CR41","volume-title":"The art of software testing","author":"GJ Myers","year":"1979","unstructured":"Myers GJ (1979) The art of software testing. Wiley, New York"},{"key":"65_CR42","series-title":"LNCS","volume-title":"TACAS\u201901","author":"B Nielsen","year":"2001","unstructured":"Nielsen B, Skou A (2001) Automated test generation from timed automata. In: TACAS\u201901. LNCS, vol\u00a02031. Springer, Berlin"},{"key":"65_CR43","unstructured":"Peleska J (2002) Formal methods for test automation\u2014hard real-time testing of controllers for the airbus aircraft family. In: IDPT\u201902"},{"issue":"1\u20132","key":"65_CR44","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1023\/A:1008387132377","volume":"10","author":"A Puri","year":"2000","unstructured":"Puri A (2000) Dynamical properties of timed automata. Discrete Event Dyn Syst 10(1\u20132):87\u2013113","journal-title":"Discrete Event Dyn Syst"},{"key":"65_CR45","series-title":"LNCS","volume-title":"13th Annual symposium on theoretical aspects of computer science, STACS\u201996","author":"J Sifakis","year":"1996","unstructured":"Sifakis J, Yovine S (1996) Compositional specification of timed systems. In: 13th Annual symposium on theoretical aspects of computer science, STACS\u201996. LNCS, vol 1046. Springer, Berlin"},{"key":"65_CR46","doi-asserted-by":"crossref","unstructured":"Springintveld J, Vaandrager F, D\u2019Argenio P (2001) Testing timed automata. Theor Comput Sci 254","DOI":"10.1016\/S0304-3975(99)00134-6"},{"key":"65_CR47","series-title":"LNCS","volume-title":"CONCUR\u201999","author":"J Tretmans","year":"1999","unstructured":"Tretmans J (1999) Testing concurrent systems: a formal approach. In: CONCUR\u201999. LNCS, vol 1664. Springer, Berlin"},{"key":"65_CR48","volume-title":"Testing techniques. Lecture notes","author":"J Tretmans","year":"2002","unstructured":"Tretmans J (2002) Testing techniques. Lecture notes. University of Twente, The Netherlands"},{"key":"65_CR49","series-title":"LNCS","volume-title":"Formal techniques in real time and fault tolerant systems (FTRTFT\u201902)","author":"S Tripakis","year":"2002","unstructured":"Tripakis S (2002) Fault diagnosis for timed automata. In: Formal techniques in real time and fault tolerant systems (FTRTFT\u201902). LNCS, vol 2469. Springer, Berlin"},{"key":"65_CR50","series-title":"LNCS","volume-title":"Formal modeling and analysis of timed systems (FORMATS\u201903)","author":"S Tripakis","year":"2004","unstructured":"Tripakis S (2004) Folk theorems on the determinization and minimization of timed automata. In: Formal modeling and analysis of timed systems (FORMATS\u201903). LNCS, vol 2791. Springer, Berlin"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-009-0065-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-009-0065-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-009-0065-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,24]],"date-time":"2023-05-24T01:19:11Z","timestamp":1684891151000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-009-0065-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,2,14]]},"references-count":50,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2009,6]]}},"alternative-id":["65"],"URL":"https:\/\/doi.org\/10.1007\/s10703-009-0065-1","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,2,14]]}}}