{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,19]],"date-time":"2025-10-19T15:40:06Z","timestamp":1760888406652,"version":"3.37.0"},"publisher-location":"Berlin, Heidelberg","reference-count":46,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642050305"},{"type":"electronic","value":"9783642050312"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-05031-2_1","type":"book-chapter","created":{"date-parts":[[2009,11,2]],"date-time":"2009-11-02T12:32:25Z","timestamp":1257165145000},"page":"1-15","source":"Crossref","is-referenced-by-count":8,"title":["Testing Real-Time Systems Using TINA"],"prefix":"10.1007","author":[{"given":"Noureddine","family":"Adjir","sequence":"first","affiliation":[]},{"given":"Pierre","family":"De Saqui-Sannes","sequence":"additional","affiliation":[]},{"given":"Kamel Mustapha","family":"Rahmouni","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"1_CR1","unstructured":"Adjir, N., De Saqui-Sanne, P., Rahmouni, M.K.: G\u00e9n\u00e9ration des s\u00e9quences de test temporis\u00e9s \u00e0 partir des r\u00e9seaux de Petri temporels \u00e0 chronom\u00e8tres. In: NOTERE 2007, Maroc."},{"issue":"2","key":"1_CR2","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science\u00a0126(2), 183\u2013235 (1994)","journal-title":"Theoretical Computer Science"},{"key":"1_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/11603009_17","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"B. B\u00e9rard","year":"2005","unstructured":"B\u00e9rard, B., Cassez, F., Haddad, S., Roux, O.H., et Lime, D.: Comparison of the Expressiveness of Timed Automata and Time Petri Nets. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol.\u00a03829, pp. 211\u2013225. Springer, Heidelberg (2005)"},{"key":"1_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/11590156_22","volume-title":"FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science","author":"B. B\u00e9rard","year":"2005","unstructured":"B\u00e9rard, B., Cassez, F., Haddad, S., Lime, D., Roux, O.H.: When are timed automata weakly timed bisimilar to time Petri nets? In: Sarukkai, S., Sen, S. (eds.) FSTTCS 2005. LNCS, vol.\u00a03821, pp. 273\u2013284. Springer, Heidelberg (2005)"},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"Berthomieu, B., Diaz, M.: Modelling and verification of time dependent systems using time Petri nets. IEEE transactions on software Engineering\u00a017(3) (1991)","DOI":"10.1109\/32.75415"},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"Berthomieu, B., Ribet, P.O., Vernadat, F.: The tool TINA \u2013 Construction of Abstract State Spaces for Petri Nets and Time Petri Nets. Inter. JPR\u00a042(14) (July 2004)","DOI":"10.1080\/00207540412331312688"},{"key":"1_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/11867340_7","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"B. Berthomieu","year":"2006","unstructured":"Berthomieu, B., Peres, F., Vernadat, F.: Bridging the gap between Timed Automata and Bounded Time Petri Nets. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol.\u00a04202, pp. 82\u201397. Springer, Heidelberg (2006)"},{"key":"1_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"523","DOI":"10.1007\/978-3-540-75596-8_37","volume-title":"Automated Technology for Verification and Analysis","author":"B. Berthomieu","year":"2007","unstructured":"Berthomieu, B., Peres, F., Vernadat, F.: Model Checking Bounded Prioritized Time Petri Nets. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol.\u00a04762, pp. 523\u2013532. Springer, Heidelberg (2007)"},{"issue":"14","key":"1_CR9","doi-asserted-by":"publisher","first-page":"2741","DOI":"10.1080\/00207540412331312688","volume":"42","author":"B. Berthomieu","year":"2004","unstructured":"Berthomieu, B., Ribet, P.-O., Vernadat, F.: The tool TINA \u2013construction of abstract state spaces for Petri nets and time Petri nets. IJPR\u00a042(14), 2741\u20132756 (2004)","journal-title":"IJPR"},{"key":"1_CR10","volume-title":"Handbook of Real-Time and Embedded Systems","author":"B. Berthomieu","year":"2007","unstructured":"Berthomieu, B., et Vernadat, F.: State Space Abstractions for Time Petri Nets. In: Handbook of Real-Time and Embedded Systems. CRC Press, Boca Raton (2007)"},{"issue":"2\u20133","key":"1_CR11","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1016\/j.tcs.2004.04.003","volume":"321","author":"P. Bouyer","year":"2004","unstructured":"Bouyer, P., Dufourd, C., Fleury, E., Petit, A.: Updatable timed automata. TCS\u00a0321(2\u20133), 291\u2013345 (2004)","journal-title":"TCS"},{"issue":"3","key":"1_CR12","first-page":"281","volume":"24","author":"P. Bouyer","year":"2004","unstructured":"Bouyer, P.: Forward Analysis of Updatable Timed Automata. FMSD\u00a024(3), 281\u2013320 (2004)","journal-title":"FMSD"},{"key":"1_CR13","unstructured":"Bouyer, P., Chevalier, F.: On conciseness of extensions of timed automata. JALC (2005)"},{"key":"1_CR14","first-page":"91","volume-title":"ACSD 2006","author":"P. Bouyer","year":"2006","unstructured":"Bouyer, P., Serge, H., Reynie, P.A.: Extended Timed Automata and Time Petri Nets. In: ACSD 2006, Turku, Finland, pp. 91\u2013100. IEEE Computer Society Press, Los Alamitos (2006)"},{"key":"1_CR15","unstructured":"Braberman, V., Felder, M., Marre, M.: Testing timing behaviour of real-time software. In: Intern. Software Quality Week (1997)"},{"key":"1_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/3-540-45510-8_9","volume-title":"Modeling and Verification of Parallel Processes","author":"E. Brinksma","year":"2001","unstructured":"Brinksma, E., Tretmans, J.: Testing transition systems: An annotated bibliography. In: Cassez, F., Jard, C., Rozoy, B., Dermot, M. (eds.) MOVEP 2000. LNCS, vol.\u00a02067, p. 187. Springer, Heidelberg (2001)"},{"key":"1_CR17","volume-title":"ISSTA 2002","author":"R. Cardell-Oliver","year":"2002","unstructured":"Cardell-Oliver, R.: Conformance test experiments for distributed real-time systems. In: ISSTA 2002. ACM Press, New York (2002)"},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"Cassez, F., Roux, O.H.: Structural translation from time Petri nets to timed automata. In: JSS 2006 (2006)","DOI":"10.1016\/j.jss.2005.12.021"},{"key":"1_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/978-3-540-24756-2_8","volume-title":"Integrated Formal Methods","author":"S. Chaki","year":"2004","unstructured":"Chaki, S., Clarke, E.M., Ouaknine, J., Sharygina, N., Sinha, N.: State\/Event-based Software Model Checking. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol.\u00a02999, pp. 128\u2013147. Springer, Heidelberg (2004)"},{"issue":"4","key":"1_CR20","first-page":"371","volume":"5","author":"C. Choffrut","year":"2000","unstructured":"Choffrut, C., Goldwurm, M.: Timed automata with periodic clock constraints. JALC\u00a05(4), 371\u2013404 (2000)","journal-title":"JALC"},{"key":"1_CR21","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF01211314","volume":"5","author":"R. Cleaveland","year":"1993","unstructured":"Cleaveland, R., Hennessy, M.: Testing Equivalence as a Bisimulation Equivalence. Formal Aspects of Computing\u00a05, 1\u201320 (1993)","journal-title":"Formal Aspects of Computing"},{"key":"1_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/11867340_10","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"A. David","year":"2006","unstructured":"David, A., Hakansson, J., Larsen, K.G.: Model checking timed automata with priorities using DBM subtraction. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol.\u00a04202, pp. 128\u2013142. Springer, Heidelberg (2006)"},{"key":"1_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1007\/BFb0055641","volume-title":"CONCUR \u201998 Concurrency Theory","author":"F. Demichelis","year":"1998","unstructured":"Demichelis, F., Zielonka, W.: Controlled timed automata. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol.\u00a01466, pp. 455\u2013469. Springer, Heidelberg (1998)"},{"issue":"4","key":"1_CR24","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/s100090050044","volume":"2","author":"R. Vries de","year":"2000","unstructured":"de Vries, R., Tretmans, J.: On-the-fly conformance testing using SPIN. STTT\u00a02(4), 382\u2013393 (2000)","journal-title":"STTT"},{"key":"1_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1007\/BFb0023491","volume-title":"STACS 97","author":"V. Diekert","year":"1997","unstructured":"Diekert, V., Gastin, P., Petit, A.: Removing epsilon-Transitions in Timed Automata. In: Reischuk, R., Morvan, M. (eds.) STACS 1997. LNCS, vol.\u00a01200, pp. 583\u2013594. Springer, Heidelberg (1997)"},{"key":"1_CR26","volume-title":"RTSS 1998","author":"A. En-Nouaary","year":"1998","unstructured":"En-Nouaary, A., Dssouli, R., Khendek, F., Elqortobi, A.: Timed test cases generation based on state characterization technique. In: RTSS 1998. IEEE, Los Alamitos (1998)"},{"key":"1_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/3-540-46002-0_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Fersman","year":"2002","unstructured":"Fersman, E., Pettersson, P., Yi, W.: Timed automata with asynchronous processes: Schedulability and decidability. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, pp. 67\u201382. Springer, Heidelberg (2002)"},{"key":"1_CR28","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"J.C. Fernandez","year":"1996","unstructured":"Fernandez, J.C., Jard, C., J\u00e9ron, T., Viho, G.: Using on-the-fly verification techniques for the generation of test suites. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102. Springer, Heidelberg (1996)"},{"key":"1_CR29","volume-title":"R\u00e9seaux de Petri P-temporels: contribution \u00e0 l\u2019\u00e9tude des syst\u00e8mes \u00e0 \u00e9v\u00e9nements discrets","author":"W. Khansa","year":"1997","unstructured":"Khansa, W.: R\u00e9seaux de Petri P-temporels: contribution \u00e0 l\u2019\u00e9tude des syst\u00e8mes \u00e0 \u00e9v\u00e9nements discrets. universit\u00e9 de Savoie, Annecy (1997)"},{"key":"1_CR30","first-page":"278","volume-title":"Proc. LICS 1996","author":"T.A. Henzinger","year":"1996","unstructured":"Henzinger, T.A.: The theory of hybrid automata. In: Proc. LICS 1996, pp. 278\u2013292. IEEE CSP, Los Alamitos (1996)"},{"key":"1_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-540-24617-6_9","volume-title":"Formal Approaches to Software Testing","author":"A. Hessel","year":"2004","unstructured":"Hessel, A., Larsen, K.G., Nielsen, B., Pettersson, P., Skou, A.: Time-optimal real-time test case generation using UPPAAL. In: Petrenko, A., Ulrich, A. (eds.) FATES 2003. LNCS, vol.\u00a02931, pp. 114\u2013130. Springer, Heidelberg (2004)"},{"key":"1_CR32","volume-title":"IFIP Int\u2019l Work, Test Comm. System","author":"T. Higashino","year":"1999","unstructured":"Higashino, T., Nakata, A., Taniguchi, K., Cavalli, A.: Generating test cases for a timed I\/O automaton model. In: IFIP Int\u2019l Work, Test Comm. System. Kluwer, Dordrecht (1999)"},{"key":"1_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/3-540-48683-6_12","volume-title":"Computer Aided Verification","author":"T. J\u00e9ron","year":"1999","unstructured":"J\u00e9ron, T., Morel, P.: Test generation derived from model-checking. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 108\u2013121. Springer, Heidelberg (1999)"},{"key":"1_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"470","DOI":"10.1007\/3-540-46002-0_34","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. J\u00e9ron","year":"2002","unstructured":"J\u00e9ron, T., Rusu, V., Zinovieva, E.: STG: A symbolic test generation tool. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, p. 470. Springer, Heidelberg (2002)"},{"key":"1_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-540-24617-6_10","volume-title":"Formal Approaches to Software Testing","author":"A. Khoumsi","year":"2004","unstructured":"Khoumsi, A., J\u00e9ron, T., Marchand, H.: Test cases generation for nondeterministic real-time systems. In: Petrenko, A., Ulrich, A. (eds.) FATES 2003. LNCS, vol.\u00a02931, pp. 131\u2013146. Springer, Heidelberg (2004)"},{"key":"1_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1007\/11430230_15","volume-title":"17th IFIP Intl. TestCom 2005","author":"M. Krichen","year":"2005","unstructured":"Krichen, M., Tripakis, S.: An Expressive and Implementable Formal Framework for Testing Real Time Systems. In: Khendek, F., Dssouli, R. (eds.) TestCom 2005. LNCS, vol.\u00a03502, pp. 209\u2013225. Springer, Heidelberg (2005)"},{"key":"1_CR37","first-page":"124","volume-title":"PNPM 2003","author":"D. Lime","year":"2003","unstructured":"Lime, D., Roux, O.: State class timed automaton of a time Petri net. In: PNPM 2003, Urbana, USA, pp. 124\u2013133. IEEE computer society, Los Alamitos (2003)"},{"issue":"3","key":"1_CR38","first-page":"151","volume":"22","author":"J.C. Lin","year":"2000","unstructured":"Lin, J.C., Ho, I.: Generating Real-Time Software Test Cases by Time Petri Nets. IJCA (EI journal)\u00a022(3), 151\u2013158 (2000)","journal-title":"IJCA (EI journal)"},{"issue":"9","key":"1_CR39","doi-asserted-by":"publisher","first-page":"1036","DOI":"10.1109\/TCOM.1976.1093424","volume":"24","author":"P.M. Merlin","year":"1976","unstructured":"Merlin, P.M., Farber, J.: Recoverability of communication protocols: Implications of a theoretical study. IEEE Trans. Com.\u00a024(9), 1036\u20131043 (1976)","journal-title":"IEEE Trans. Com."},{"key":"1_CR40","doi-asserted-by":"crossref","unstructured":"Mikucionis, M., Larsen, K.G., Nielsen, B.: T-UPPAAL: Online Model-based Testing of Real-time Systems. In: 19th IEEE Internat. Conf. ASE, Linz, Austria, pp. 396\u2013397 (2004)","DOI":"10.1109\/ASE.2004.1342774"},{"key":"1_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/3-540-45319-9_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B. Nielsen","year":"2001","unstructured":"Nielsen, B., Skou, A.: Automated test generation from timed automata. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, p. 343. Springer, Heidelberg (2001)"},{"key":"1_CR42","unstructured":"Peleska, J.: Formal methods for test automation hard real time testing of controllers for the airbus aircraft family. In: IDPT 2002 (2002)"},{"key":"1_CR43","unstructured":"Ramchadani, C.: Analysis of asynchronous concurrent systems by timed Petri nets, Cambridge, Mass, MIT, dept Electrical Engineering, Phd thesis (1992)"},{"key":"1_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"370","DOI":"10.1007\/11562948_28","volume-title":"Automated Technology for Verification and Analysis","author":"S.-W. Lin","year":"2005","unstructured":"Lin, S.-W., Hsiung, P.-A., Huang, C.-H., Chen, Y.-R.: Model checking prioritized timed automata. In: Peled, D.A., Tsay, Y.-K. (eds.) ATVA 2005. LNCS, vol.\u00a03707, pp. 370\u2013384. Springer, Heidelberg (2005)"},{"key":"1_CR45","doi-asserted-by":"crossref","unstructured":"Springintveld, J., Vaandrager, F., D\u2019Argenio, P.: Testing timed automata. TCS\u00a0254 (2001)","DOI":"10.1016\/S0304-3975(99)00134-6"},{"key":"1_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/3-540-48320-9_6","volume-title":"CONCUR\u201999. Concurrency Theory","author":"J. Tretmans","year":"1999","unstructured":"Tretmans, J.: Testing concurrent systems: A formal approach. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol.\u00a01664, pp. 46\u201365. Springer, Heidelberg (1999)"}],"container-title":["Lecture Notes in Computer Science","Testing of Software and Communication Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-05031-2_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,13]],"date-time":"2025-02-13T01:25:13Z","timestamp":1739409913000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-05031-2_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642050305","9783642050312"],"references-count":46,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-05031-2_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}