{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,12]],"date-time":"2026-03-12T14:04:49Z","timestamp":1773324289923,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540242871","type":"print"},{"value":"9783540305699","type":"electronic"}],"license":[{"start":{"date-parts":[[2005,1,1]],"date-time":"2005-01-01T00:00:00Z","timestamp":1104537600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-30569-9_4","type":"book-chapter","created":{"date-parts":[[2010,7,4]],"date-time":"2010-07-04T17:59:08Z","timestamp":1278266348000},"page":"70-85","source":"Crossref","is-referenced-by-count":11,"title":["Mastering Test Generation from Smart Card Software Formal Models"],"prefix":"10.1007","author":[{"given":"Fabrice","family":"Bouquet","sequence":"first","affiliation":[]},{"given":"Bruno","family":"Legeard","sequence":"additional","affiliation":[]},{"given":"Fabien","family":"Peureux","sequence":"additional","affiliation":[]},{"given":"Eric","family":"Torreborre","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","unstructured":"European Telecommunications Standards Institute, F-06921 Sophia Antipolis cedex - France. GSM 11-11 V7.2.0 Technical Specifications (1999)"},{"key":"4_CR2","unstructured":"European Telecommunications Standards Institute, F-06921 Sophia Antipolis cedex - France. ETSI TS 102 221 V4.4.0 Technical Specifications (2001)"},{"key":"4_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/BFb0024651","volume-title":"FME \u201993: Industrial-Strength Formal Methods","author":"J. Dick","year":"1993","unstructured":"Dick, J., Faivre, A.: Automating the generation and sequencing of test cases from model-based specifications. In: Larsen, P.G., Woodcock, J.C.P. (eds.) FME 1993. LNCS, vol.\u00a0670, pp. 268\u2013284. Springer, Heidelberg (1993)"},{"key":"4_CR4","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1109\/ICSE.1993.346025","volume-title":"Proceedings of the 15th International Conference on Software Engineering (ICSE 1993)","author":"P. Stocks","year":"1993","unstructured":"Stocks, P., Carrington, D.A.: Test templates: a specification-based testing framework. In: Proceedings of the 15th International Conference on Software Engineering (ICSE 1993), Baltimore, Maryland, May 1993, pp. 405\u2013414. IEEE Computer Society Press, Los Alamitos (1993)"},{"key":"4_CR5","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1002\/(SICI)1099-1689(199703)7:1<19::AID-STVR124>3.0.CO;2-N","volume":"7","author":"R. Hierons","year":"1997","unstructured":"Hierons, R.: Testing from a Z specification. The Journal of Software Testing, Verification and Reliability\u00a07, 19\u201333 (1997)","journal-title":"The Journal of Software Testing, Verification and Reliability"},{"key":"4_CR6","unstructured":"Van Aertryck, L., Benveniste, M., Le Metayer, D.: CASTING: a formally based software test generation method. In: 1st IEEE International Conference on Formal Engineering Methods (ICFEM 1997), pp. 99\u2013112 (1997)"},{"key":"4_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1007\/3-540-48119-2_29","volume-title":"FM\u201999 - Formal Methods","author":"S. Behnia","year":"1999","unstructured":"Behnia, S., Waeselynck, H.: Test criteria definition for B models. In: Wing, J.M., Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol.\u00a01708, pp. 509\u2013529. Springer, Heidelberg (1999)"},{"key":"4_CR8","unstructured":"Object Management Group. UML Standard (2003), \n                  \n                    http:\/\/www.omg.org"},{"key":"4_CR9","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-BOOK: Assigning Programs to Meanings","author":"J.-R. Abrial","year":"1996","unstructured":"Abrial, J.-R.: The B-BOOK: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996) ISBN 0_521_49619_5"},{"key":"4_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/3-540-45418-7_6","volume-title":"Smart Card Programming and Security","author":"D. Clarke","year":"2001","unstructured":"Clarke, D., J\u00e9ron, T., Rusu, V., Zinovieva, E.: Automated test and oracle generation for smart-card applications. In: Attali, S., Jensen, T. (eds.) E-smart 2001. LNCS, vol.\u00a02140, pp. 58\u201370. Springer, Heidelberg (2001)"},{"issue":"10","key":"4_CR11","doi-asserted-by":"crossref","first-page":"915","DOI":"10.1002\/spe.597","volume":"34","author":"E. Bernard","year":"2004","unstructured":"Bernard, E., Legeard, B., Luck, X., Peureux, F.: Generation of test sequences from formal specifications: GSM 11. 11 standard case-study. The Journal of Software Practice and Experience\u00a034(10), 915\u2013948 (2004)","journal-title":"11 standard case-study. The Journal of Software Practice and Experience"},{"key":"4_CR12","series-title":"ENTCS","volume-title":"Proceedings of the 8th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2003)","author":"J. Philipps","year":"2003","unstructured":"Philipps, J., Pretschner, A., Slotosch, O., Aiglstorfer, E., Kriebel, S., Scholl, K.: Model-based test case generation for smart cards. In: Proceedings of the 8th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2003), Trondheim, Norway, June 2003. ENTCS, vol.\u00a080. Elsevier, Amsterdam (2003)"},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"778","DOI":"10.1007\/978-3-540-45236-2_42","volume-title":"FME 2003: Formal Methods","author":"F. Bouquet","year":"2003","unstructured":"Bouquet, F., Legeard, B.: Reification of executable test scripts in formal specification-based test generation: the Java Card transaction mechanism case study. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805, pp. 778\u2013795. Springer, Heidelberg (2003)"},{"key":"4_CR14","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1109\/ASE.2001.989833","volume-title":"Proceedings of the 16th International Conference on Automated Software Engineering (ASE 2001)","author":"B. Legeard","year":"2001","unstructured":"Legeard, B., Peureux, F.: Generation of functional test sequences from B formal specifications - Presentation and industrial case-study. In: Proceedings of the 16th International Conference on Automated Software Engineering (ASE 2001), San Diego, USA, November 2001, pp. 377\u2013381. IEEE Computer Society Press, Los Alamitos (2001)"},{"key":"4_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/3-540-45648-1_16","volume-title":"ZB 2002: Formal Specification and Development in Z and B","author":"B. Legeard","year":"2002","unstructured":"Legeard, B., Peureux, F., Utting, M.: A comparison of the BTT and TTF test-generation methods. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol.\u00a02272, pp. 309\u2013329. Springer, Heidelberg (2002)"},{"key":"4_CR16","volume-title":"Black-Box Testing: Techniques for Functional Testing of Software and Systems","author":"B. Beizer","year":"1995","unstructured":"Beizer, B.: Black-Box Testing: Techniques for Functional Testing of Software and Systems. John Wiley & Sons, New York (1995)"},{"key":"4_CR17","unstructured":"Ambert, F., Bouquet, F., Legeard, B., Peureux, F.: Automated boundary-value test generation from specifications - method and tools. In: Proceedings of the 4th International Conference on Software Testing (ICS-Test 2003), K\u00f6ln, Germany, April 2003. Software and Systems Quality Conferences, pp. 52\u201368 (2003)"},{"key":"4_CR18","unstructured":"Statemate Tool (2003), \n                  \n                    http:\/\/www.ilogix.com"},{"key":"4_CR19","unstructured":"Ambert, F., Bouquet, F., Chemin, S., Guenaud, S., Legeard, B., Peureux, F., Vacelet, N., Utting, M.: BZ-TT: A tool-set for test generation from Z and B using constraint logic programming. In: Proceedings of the CONCUR 2002 Workshop on Formal Approaches to Testing of Software (FATES 2002), Brn0\u0308, Czech Republic, August, pp. 105\u2013120 (2002) INRIA Technical Report"},{"issue":"4","key":"4_CR20","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1145\/267580.267590","volume":"29","author":"H. Zhu","year":"1997","unstructured":"Zhu, H., Hall, P.A.V., May, J.H.R.: Software Unit Test Coverage and Adequacy. ACM Computing Surveys\u00a029(4), 366\u2013427 (1997)","journal-title":"ACM Computing Surveys"},{"key":"4_CR21","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1145\/143062.143100","volume-title":"Proceedings of the 14th International Conference on Software Engineering (ICSE 1992)","author":"D.J. Richardson","year":"1992","unstructured":"Richardson, D.J., Aha, S.L., O\u2019Malley, T.O.: Specification-based test oracles for reactive systems. In: Proceedings of the 14th International Conference on Software Engineering (ICSE 1992), Melbourne, Australia, May 1992, pp. 105\u2013118. ACM Press, New York (1992)"},{"issue":"2","key":"4_CR22","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1002\/stvr.287","volume":"14","author":"B. Legeard","year":"2004","unstructured":"Legeard, B., Peureux, F., Utting, M.: Controlling Test Case Explosion in Test Generation from B Formal Models. The Journal of Software Testing, Verification and Reliability\u00a014(2), 81\u2013103 (2004)","journal-title":"The Journal of Software Testing, Verification and Reliability"},{"key":"4_CR23","unstructured":"ISO. Information Processing Systems, Open Systems Interconnection. OSI Conformance Testing Methodology and Framework \u2013 ISO 9646 (1998)"}],"container-title":["Lecture Notes in Computer Science","Construction and Analysis of Safe, Secure, and Interoperable Smart Devices"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30569-9_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T19:34:42Z","timestamp":1558294482000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30569-9_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540242871","9783540305699"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30569-9_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}