{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,28]],"date-time":"2022-03-28T21:56:54Z","timestamp":1648504614822},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2006,6,1]],"date-time":"2006-06-01T00:00:00Z","timestamp":1149120000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/2.0"},{"start":{"date-parts":[[2006,6,1]],"date-time":"2006-06-01T00:00:00Z","timestamp":1149120000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/2.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Braz Comp Soc"],"published-print":{"date-parts":[[2006,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Test synthesis (or test generation) can be described as follows: from a formal specification of an implementation under test (<jats:bold><jats:italic>IUT<\/jats:italic><\/jats:bold>), and from a test purpose describing behaviors to be tested, the aim is to synthesize test cases to be executed in order to check whether the<jats:bold><jats:italic>IUT<\/jats:italic><\/jats:bold>conforms to its formal specification, while trying to control the<jats:bold><jats:italic>IUT<\/jats:italic><\/jats:bold>so that it satisfies the test purpose. In this paper, we study the synthesis of test cases for symbolic real-time systems. By symbolic, we mean that the specification of the<jats:bold><jats:italic>IUT<\/jats:italic><\/jats:bold>contains variables and parameters. And by realtime, we mean that the specification of the<jats:bold><jats:italic>IUT<\/jats:italic><\/jats:bold>contains timing constraints. Our method combines and generalizes two testing methods presented in previous work, namely: 1) a method for synthesizing test cases for (non-symbolic) real-time systems, and 2) a method for synthesizing test cases for (non-real-time) symbolic systems.<\/jats:p>","DOI":"10.1007\/bf03192393","type":"journal-article","created":{"date-parts":[[2010,11,12]],"date-time":"2010-11-12T04:48:02Z","timestamp":1289537282000},"page":"31-48","source":"Crossref","is-referenced-by-count":1,"title":["On synthesizing test cases in symbolic real-time testing"],"prefix":"10.1007","volume":"12","author":[{"given":"Ahmed","family":"Khoumsi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"BF03192393_CR1","unstructured":"ISO\/IEC.International Standard 9646-1\/2\/3, OSI-Open Systems Interconnection, Information Technology \u2014 Open Systems Interconnection Conformance Testing Methodology and Framework, 1992."},{"key":"BF03192393_CR2","volume-title":"Testing real-time constraints","author":"D. Clarke","year":"1996","unstructured":"D. Clarke.Testing real-time constraints. PhD thesis, Department of Computer and Information Science, University of Pennsylvania USA1996."},{"key":"BF03192393_CR3","series-title":"Technical Report CTIT97-17","volume-title":"Testing timed automata","author":"J. Springintveld","year":"1997","unstructured":"J. Springintveld, F. Vaandrager, and P. D\u2019Argenio. Testing timed automata. Technical Report CTIT97-17, University of TwenteAmsterdam, The Netherlands, 1997."},{"key":"BF03192393_CR4","unstructured":"V. Braberman, M. Felder, and M. Mass\u00e9. Testing timing behaviors of real time software. InProc. Quality Week 1997, pages 143\u2013155, San Francisco, USA, April\u2013May 1997."},{"key":"BF03192393_CR5","unstructured":"J. Peleska, P. Amthor, S. Dick, O. Meyer, M. Siegel, and C. Zahlten. Testing reactive real-time systems. InProc. Mater. for the School\u20145th Intern. School and Sympos. on Form. Technique in Real-Time and Fault-Toler. Syst. (FTRTFT), Lyngby, Denmark, 1998."},{"key":"BF03192393_CR6","unstructured":"A. En-Nouaary, R. Dssouli, F. Khendek, and A. Elqortobi. Timed test generation based on state characterization technique. InProc. 19th IEEE Real-Time Systems Sympos. (RTSS), Madrid, Spain, December 1998."},{"key":"BF03192393_CR7","volume-title":"Specification and test of real-time systems","author":"B. Nielsen","year":"2000","unstructured":"B. Nielsen.Specification and test of real-time systems. PhD thesis, Dept of Comput. Science, Faculty of Engin. and Sc., Aalborg University, Aalborg, Denmark, 2000."},{"key":"BF03192393_CR8","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1007\/s001650070009","volume":"12","author":"R. Cardell-Oliver","year":"2000","unstructured":"R. Cardell-Oliver. Conformance testing of real-time systems with timed automata.Formal Aspects of Computing, 12:350\u2013371, 2000.","journal-title":"Formal Aspects of Computing"},{"key":"BF03192393_CR9","doi-asserted-by":"crossref","unstructured":"R. Cardell-Oliver. Conformance testing of real-time systems with timed automata. InNordic Workshop on Programming Theory, October 2000.","DOI":"10.1007\/s001650070009"},{"key":"BF03192393_CR10","doi-asserted-by":"crossref","unstructured":"A. Khoumsi. A method for testing the conformance of real time systems. InProc. 7th Intern. Sympos. on Formal Techn. in Real-Time and Fault Toler. Systems (FTRTFT), Oldenburg, Germany, September 2002.","DOI":"10.1007\/3-540-45739-9_20"},{"key":"BF03192393_CR11","volume-title":"Proc. Formal Approaches to TEsting of Software (FATES), LNCS 2931","author":"A. Khoumsi","year":"2003","unstructured":"A. Khoumsi, T. J\u00e9ron, and H. Marchand. Test cases generation for nondeterministic real-time systems. InProc. Formal Approaches to TEsting of Software (FATES), LNCS 2931, Montreal, Canada, October 2003. Springer."},{"key":"BF03192393_CR12","doi-asserted-by":"crossref","unstructured":"M. Krichen and S. Tripakis. Black-box conformance testing for real-time systems. InProc. Model Checking Software: 11th Int. SPIN Workshop, LNCS 2989. Springer-Verlag, 2004.","DOI":"10.1007\/978-3-540-24732-6_8"},{"key":"BF03192393_CR13","doi-asserted-by":"crossref","unstructured":"V. Rusu, L. du Bousquet, and T. J\u00e9ron. An approach to symbolic test generation. InInt. Conf. on Integrating Formal Methods (IFM), pages 338\u2013357, Dagstuhl, Germany, 2000. LNCS 1945.","DOI":"10.1007\/3-540-40911-4_20"},{"key":"BF03192393_CR14","doi-asserted-by":"crossref","unstructured":"V. Rusu. Verification using test generation techniques. InFormal Methods Europe (FME), pages 252\u2013271. LNCS 2391, 2002.","DOI":"10.1007\/3-540-45614-7_15"},{"key":"BF03192393_CR15","doi-asserted-by":"crossref","unstructured":"D. Clarke, Thierry J\u00e9ron, V. Rusu, and E. Zinovieva. STG: a symbolic test generation tool. InTools and Algor. for the Const. and Anal. of Syst. (TACAS), pages 470\u2013475. LNCS 2280, 2002.","DOI":"10.1007\/3-540-46002-0_34"},{"key":"BF03192393_CR16","doi-asserted-by":"crossref","unstructured":"G. Behrmann, J. Bengtsson, A. David, K. G., Larsen, P. Pettersson, and W. Yi. Uppaal implementation secrets. InProc. Form. Technique in Real-Time and Fault-Toler. Syst. (FTRTFT), pages 3\u201322. Springer-Verlag, Sept. 2002.","DOI":"10.1007\/3-540-45739-9_1"},{"key":"BF03192393_CR17","doi-asserted-by":"crossref","unstructured":"S. Tripakis. Fault diagnosis for timed automata. InProc. Form. Technique in Real-Time and Fault-Toler. Syst. (FTRTFT), LNCS 2469. Springer-Verlag, 2002.","DOI":"10.1007\/3-540-45739-9_14"},{"key":"BF03192393_CR18","doi-asserted-by":"crossref","unstructured":"A. Khoumsi. Complete test graph generation for symbolic real-time systems. InProc. Brazilian Symposium of Formal Methods (SBMF), Recife, Brazil, November 2004. Best Paper Award.","DOI":"10.1016\/j.entcs.2005.03.006"},{"key":"BF03192393_CR19","doi-asserted-by":"crossref","unstructured":"R. Alur. Timed automata. InProc. 11th Intern. Conf. on Comp. Aided Verif. (CAV), pages 8\u201322. Springer-Verlag LNCS 1633, 1999.","DOI":"10.1007\/3-540-48683-6_3"},{"key":"BF03192393_CR20","doi-asserted-by":"crossref","unstructured":"C. Jard, T. J\u00e9ron, L. Tanguy, and C. Viho. Remote testing can be as powerful as local testing. InProc. PSTV\/FORTE, Beijing, China, October 1999.","DOI":"10.1007\/978-0-387-35578-8_2"},{"key":"BF03192393_CR21","doi-asserted-by":"crossref","unstructured":"T. J\u00e9ron, H. Marchand, V. Rusu, and V. Tschaen. Ensuring the conformance of reactive discrete-event systems using supervisory control. In42nd CDC, Hawaii, USA, December 2003.","DOI":"10.1080\/00207540410001705202"},{"key":"BF03192393_CR22","unstructured":"C. Jard and T. J\u00e9ron. TGV: theory, principles and algorithms. InProc. 6th World Conf. on Integ. Design and Process Technol. (IDPT), Pasadena, California, USA, June 2002."},{"key":"BF03192393_CR23","volume-title":"A Formal Approach to Conformance Testing","author":"J. Tretmans","year":"1992","unstructured":"J. Tretmans.A Formal Approach to Conformance Testing. PhD thesis, University of Twente, The Netherlands, December 1992."},{"key":"BF03192393_CR24","doi-asserted-by":"crossref","unstructured":"A. Khoumsi and L. Ouedraogo. A new method for transforming timed automata. InProc. Brazilian Symposium of Formal Methods (SBMF), Recife, Brazil, November 2004.","DOI":"10.1016\/j.entcs.2005.03.007"},{"key":"BF03192393_CR25","unstructured":"A. Khoumsi and M. Nourelfath. An efficient-method for the supervisory control of dense real-time discrete event systems. InProc. 8th Intern. Conf. on Real-Time Computing Systems (RTCSA), Tokyo, Japan, March 2002."},{"key":"BF03192393_CR26","unstructured":"A. Khoumsi. Supervisory control of dense real-time discrete-event systems with partial observation. InProc. 6th Intern. Workshop on Discrete Event Systems (WODES), Zaragoza, Spain, October 2002."},{"key":"BF03192393_CR27","unstructured":"A. Khoumsi. Supervisory control for the conformance of real-time discrete-event systems. InProc. 7th Intern. Workshop on Discrete Event Systems (WODES), Reims, France, September 2004."},{"key":"BF03192393_CR28","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"R. Alur and D. Dill. A theory of timed automata.Theoretical Computer Science, 126:183\u2013235, 1994.","journal-title":"Theoretical Computer Science"}],"container-title":["Journal of the Brazilian Computer Society"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/BF03192393.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/BF03192393\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/www.springerlink.com\/index\/pdf\/10.1007\/BF03192393","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/BF03192393.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,13]],"date-time":"2021-11-13T12:23:04Z","timestamp":1636806184000},"score":1,"resource":{"primary":{"URL":"https:\/\/journal-bcs.springeropen.com\/articles\/10.1007\/BF03192393"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,6]]},"references-count":28,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2006,6]]}},"alternative-id":["BF03192393"],"URL":"https:\/\/doi.org\/10.1007\/bf03192393","relation":{},"ISSN":["0104-6500","1678-4804"],"issn-type":[{"value":"0104-6500","type":"print"},{"value":"1678-4804","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,6]]}}}