{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,1]],"date-time":"2026-02-01T17:59:26Z","timestamp":1769968766952,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540662020","type":"print"},{"value":"9783540486831","type":"electronic"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48683-6_12","type":"book-chapter","created":{"date-parts":[[2007,10,7]],"date-time":"2007-10-07T03:22:18Z","timestamp":1191727338000},"page":"108-122","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":48,"title":["Test Generation Derived from Model-Checking"],"prefix":"10.1007","author":[{"given":"Thierry","family":"J\u00e9ron","sequence":"first","affiliation":[]},{"given":"Pierre","family":"Morel","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,1,14]]},"reference":[{"key":"12_CR1","unstructured":"ISO\/IEC International Standard 9646-1\/2\/3. OSI-Open Systems Interconnection, Information Technology-Open Systems Interconnection Conformance Testing Methodology and Framework, 1992. 108"},{"issue":"3","key":"12_CR2","first-page":"108","volume":"53","author":"S. Abramsky","year":"1987","unstructured":"S. Abramsky. Observational equivalence as a testing equivalence. Theoretical Computer Science, 53(3), 1987. 108","journal-title":"Theoretical Computer Science"},{"key":"12_CR3","unstructured":"B. Algayres, Y. Lejeune, F. Hugonnet, and F. Hantz. The AVALON project: A VALidatiON Environment For SDL\/MSC Descriptions. In 6th SDL Forum, Darmstadt, 1993. 118, 120"},{"key":"12_CR4","unstructured":"M. Bozga, J.-C. Fernandez, L. Ghirvu, C. Jard, T. J\u00e9ron, A. Kerbrat, P. Morel, and L. Mounier. Verification and test generation for the SSCOP protocol. Journal of Science of Computer Programming, Special Issue on The Application of Formal Methods in Industrial Critical Systems, To appear, 1999. 117, 118"},{"key":"12_CR5","unstructured":"E. Brinskma. A theory for the derivation of tests. In Protocol Specification, Testing and Verification VIII, pages 63\u201374. North-Holland, 1988. 108"},{"issue":"8","key":"12_CR6","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"2","author":"E.M. Clarke","year":"1986","unstructured":"E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite state concurrent systems using temporal logic specification. ACM Transactions on Programming Languages and Systems, 2(8):244\u2013263, 1986. 109","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"12_CR7","series-title":"Lect Notes Comput Sci","volume-title":"Workshop on Computer Aided Verification","author":"C. Courcoubetis","year":"1990","unstructured":"C. Courcoubetis, M. Vardi, P. Wolper, and M. Yannakakis. Memory efficient algorithms for the verification of temporal properties. In Workshop on Computer Aided Verification. LNCS 531, June 1990. 109"},{"key":"12_CR8","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1016\/0304-3975(84)90113-0","volume":"34","author":"R. Nicola De","year":"1984","unstructured":"R. De Nicola and M. Henessy. Testing equivalences for processes. Theoretical Computer Science, 34:83\u2013133, 1984. 108","journal-title":"Theoretical Computer Science"},{"key":"12_CR9","unstructured":"R.G. De Vries and J. Tretmans. On-the-Fly Conformance Testing using Spin. In G. Holzmann, E. Najm, and A. Serhrouchni, editors, Fourth Workshop on Automata Theoretic Verification with the Spin Model Checker, ENST 98 S 002, pages 115\u2013128, Paris, France, November 2 1998. 119"},{"key":"12_CR10","series-title":"Lect Notes Comput Sci","volume-title":"Third Workshop TACAS, Enschede, The Netherlands","author":"A. Engels","year":"1997","unstructured":"A. Engels, L. Feijs, and S. Mauw. Test generation for intelligent networks using model checking. In Third Workshop TACAS, Enschede, The Netherlands, LNCS 1217. Springer-Verlag, 1997. 109"},{"key":"12_CR11","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of CAV\u201996 (New Brunswick, New Jersey, USA)","author":"J.-C. Fernandez","year":"1996","unstructured":"J.-C. Fernandez, H. Garavel, A. Kerbrat, R. Mateescu, L. Mounier, and M. Sighireanu. CADP: A Protocol Validation and Verification Toolbox. In Rajeev Alur and Thomas A. Henzinger, editors, Proc. of CAV\u201996 (New Brunswick, New Jersey, USA). LNCS 1102, August 1996. 118"},{"key":"12_CR12","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of CAV\u201996, (New Brunswick, New Jersey, USA)","author":"J.-C. Fernandez","year":"1996","unstructured":"J.-C. Fernandez, C. Jard, T. J\u00e9ron, and C. Viho. Using On-the-fly Verification Techniques for the Generation of Test Suites. In R. Alur and T.A. Henzinger, editors, Proc. of CAV\u201996, (New Brunswick, New Jersey, USA). LNCS 1102, August 1996. 109, 117, 118"},{"key":"12_CR13","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/S0167-6423(96)00032-9","volume":"29","author":"J.-C. Fernandez","year":"1997","unstructured":"J.-C. Fernandez, C. Jard, T. J\u00e9ron, and C. Viho. An Experiment in Automatic Generation of Test Suites for Protocoles with Verification Technology. Science of Computer Programming, 29, 1997. 109, 117, 118","journal-title":"Science of Computer Programming"},{"key":"12_CR14","first-page":"253","volume-title":"6th SDL Forum","author":"J. Grabowski","year":"1993","unstructured":"J. Grabowski, D. Hogrefe, and R. Nahm. Test case generation with test purpose specification by MSCs. In O. F\u00e6rgemand and A. Sarma, editors, 6th SDL Forum, pages 253\u2013266, Darmstadt (Germany), 1993. Elsevier Science B.V. (North-Holland). 119"},{"key":"12_CR15","unstructured":"J.E. Hopcroft and J.D. Ullman. Introduction to automata theory, languages, and computation. Addison-Wesley series in computer science, 1979. 118"},{"key":"12_CR16","unstructured":"ITU-T SG 10\/Q.8 ISO\/IEC JTC1\/SC21 WG7. Information retrieval, transfer and management for OSI; framework: Formal Methods in Conformance Testing. CD 13245-1, ITU-T proposed recommendation Z500. ISO\/ITU-T, 1996. 108"},{"key":"12_CR17","unstructured":"T. J\u00e9ron and P. Morel. DeAbstraction, \u03c4-r\u00e9duction et d\u00e9terminisation \u00e0 la vol\u00e9e: application \u00e0 la g\u00e9n\u00e9ration de test. In G. Leduc, editor, CFIP\u201997: Ing\u00e9nierie des Protocoles. Hermes, September 1997. 109, 110, 117, 118"},{"key":"12_CR18","doi-asserted-by":"crossref","unstructured":"H. Kahlouche, C. Viho, and M. Zendri. An industrial experiment in automatic generation of executable test suites for a cache coherency protocol. In A. Petrenko and N. Yevtushenko, editors, IFIP TC6 11th International Workshop on Testing of Communicating Systems. Chapman & Hall, September 1998. 118","DOI":"10.1007\/978-0-387-35381-4_13"},{"key":"12_CR19","doi-asserted-by":"crossref","unstructured":"A. Kerbrat, T. J\u00e9ron, and R. Groz. Automated Test Generation from SDL Specifications. In Proc. 9th SDL FORUM (Montral, Quebec, Canada), June 1999. 120","DOI":"10.1016\/B978-044450228-5\/50011-4"},{"key":"12_CR20","doi-asserted-by":"publisher","first-page":"1090","DOI":"10.1109\/5.533956","volume":"848","author":"D. Lee","year":"1996","unstructured":"D. Lee and M. Yannakakis. Principles and methods of testing finite state machines-a survey. Proc. of the IEEE, 84(8):1090\u20131123, August 1996. 108, 118","journal-title":"Proc. of the IEEE"},{"key":"12_CR21","unstructured":"M. Phalippou. Relations d\u2019implantations et Hypoth\u00e8ses de test sur les automates \u00e0 entres et sorties. PhD thesis, Universit\u00e9 de Bordeaux, 1994. 108"},{"key":"12_CR22","unstructured":"M. Phalippou. Test sequence generation using Estelle or SDL structure information. In FORTE\u201994, Berne, October 1994. 120"},{"key":"12_CR23","doi-asserted-by":"crossref","unstructured":"A. Pnueli. The temporal logic of programs. In Proc. of the 18th Symposium on the Foundations of Computer Science. ACM, November 1977. 109","DOI":"10.1109\/SFCS.1977.32"},{"issue":"2","key":"12_CR24","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1137\/0201010","volume":"1","author":"R. Tarjan","year":"1972","unstructured":"R. Tarjan. Depth-first search and linear graph algorithms. SIAM Journal Computing, 1(2):146\u2013160, June 1972. 112, 112","journal-title":"SIAM Journal Computing"},{"issue":"3","key":"12_CR25","first-page":"103","volume":"17","author":"J. Tretmans","year":"1996","unstructured":"J. Tretmans. Test generation with inputs, outputs and repetitive quiescence. Software-Concepts and Tools, 17(3):103\u2013120, 1996. 108, 110, 110, 119","journal-title":"Software-Concepts and Tools"},{"key":"12_CR26","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/3-540-57208-2_31","volume-title":"CONCUR\u2019 93","author":"B. Vergauwen","year":"1993","unstructured":"B. Vergauwen and J. Lewi. A linear local model checking algorithm for CTL. In E. Best, editor, CONCUR\u2019 93, LNCS 715, pages 447\u2013461. Springer-Verlag, 1993. 109"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48683-6_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,6]],"date-time":"2020-04-06T06:05:49Z","timestamp":1586153149000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48683-6_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540662020","9783540486831"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/3-540-48683-6_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1999]]},"assertion":[{"value":"14 January 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}