{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T14:19:55Z","timestamp":1775053195761,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540408284","type":"print"},{"value":"9783540452362","type":"electronic"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"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":[[2003]]},"DOI":"10.1007\/978-3-540-45236-2_42","type":"book-chapter","created":{"date-parts":[[2010,6,25]],"date-time":"2010-06-25T20:08:38Z","timestamp":1277496518000},"page":"778-795","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Reification of Executable Test Scripts in Formal Specification-Based Test Generation: The Java Card Transaction Mechanism Case Study"],"prefix":"10.1007","author":[{"given":"Fabrice","family":"Bouquet","sequence":"first","affiliation":[]},{"given":"Bruno","family":"Legeard","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,9,25]]},"reference":[{"key":"42_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book: Assigning Programs to Meaning","author":"J.-R. Abrial","year":"1996","unstructured":"Abrial, J.-R.: The B-Book: Assigning Programs to Meaning. Cambridge University Press, Cambridge (1996)"},{"key":"42_CR2","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 contraint logic programming. In: Hierons, R., Jerron, T. (eds.) Formal Approaches to Testing of Software, FATES 2002 workshop of CONCUR 2002, August 2002, pp. 105\u2013120. INRIA Report (2002)"},{"issue":"6","key":"42_CR3","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1049\/sej.1991.0040","volume":"6","author":"G. Bernot","year":"1991","unstructured":"Bernot, G., Gaudel, M.-C., Marre, B.: Software testing based on formal specifications: a theory and a tool. Software Engineering Journal\u00a06(6), 387\u2013405 (1991)","journal-title":"Software Engineering Journal"},{"key":"42_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/3-540-46002-0_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F. Bouquet","year":"2002","unstructured":"Bouquet, F., Legeard, B., Peureux, F.: CLPS-B \u2013 A Constraint Solver for B. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, pp. 188\u2013204. Springer, Heidelberg (2002)"},{"key":"42_CR5","unstructured":"Carrington, D., MacColl, I., McDonald, J., Murray, L., Strooper, P.: From object- Z specifications to classbench test suites. Technical Report 98\u201322, SVRC \u2013 University of Queensland (1998)"},{"key":"42_CR6","unstructured":"Clearsy. Atelier B V3, 10\/2001, \n\nhttp:\/\/www.atelierb.societe.com"},{"key":"42_CR7","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":"42_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/3-540-61474-5_82","volume-title":"Computer Aided Verification","author":"J.-C. Fernandez","year":"1996","unstructured":"Fernandez, J.-C., Jard, C., Jeron, T., Viho, C.: Using on-the-fly verification techniques for the generation of test suites. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 348\u2013359. Springer, Heidelberg (1996)"},{"key":"42_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/3-540-59293-8_188","volume-title":"TAPSOFT \u201995: Theory and Practice of Software Development","author":"M.-C. Gaudel","year":"1995","unstructured":"Gaudel, M.-C.: Testing can be formal too. In: Mosses, P.D., Schwartzbach, M.I., Nielsen, M. (eds.) CAAP 1995, FASE 1995, and TAPSOFT 1995. LNCS, vol.\u00a0915, pp. 82\u201396. Springer, Heidelberg (1995)"},{"key":"42_CR10","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":"42_CR11","unstructured":"ISO. OSI Conformance Testing Methodology and Framework \u2013 ISO 9646 (1999)"},{"key":"42_CR12","volume-title":"Systematic Software Development Using VDM","author":"C. Jones","year":"1990","unstructured":"Jones, C.: Systematic Software Development Using VDM, 2nd edn. Prentice-Hall, Englewood Cliffs (1990)","edition":"2"},{"key":"42_CR13","first-page":"377","volume-title":"16th IEEE 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 \u2013 presentation and industrial case-study. In: 16th IEEE International conference on Automated Software Engineering (ASE 2001), San Diego, USA, pp. 377\u2013381. IEEE press, Los Alamitos (2001)"},{"key":"42_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/3-540-45614-7_2","volume-title":"FME 2002: Formal Methods - Getting IT Right","author":"B. Legeard","year":"2002","unstructured":"Legeard, B., Peureux, F., Utting, M.: Automated boundary testing from Z and B. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol.\u00a02391, pp. 21\u201340. Springer, Heidelberg (2002)"},{"issue":"2","key":"42_CR15","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1002\/(SICI)1097-024X(199902)29:2<167::AID-SPE225>3.0.CO;2-V","volume":"29","author":"A. Offutt","year":"1999","unstructured":"Offutt, A., Jin, Z., Pan, J.: The dynamic domain reduction procedure for test data generation. The Journal of Software Practice and Experience\u00a029(2), 167\u2013193 (1999)","journal-title":"The Journal of Software Practice and Experience"},{"issue":"3","key":"42_CR16","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1109\/32.667877","volume":"24","author":"D.K. Peters","year":"1998","unstructured":"Peters, D.K., Parnas, D.L.: Using test oracles generated from program documentation. Software Engineering\u00a024(3), 161\u2013173 (1998)","journal-title":"Software Engineering"},{"key":"42_CR17","first-page":"105","volume-title":"Proceedings of the 14th International Conference on Software Engineering (ICSE 1992)","author":"D. Richardson","year":"1992","unstructured":"Richardson, D., O\u2019Malley, S.A.T.: 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)"},{"key":"42_CR18","volume-title":"The Z notation: A Reference Manual","author":"J. Spivey","year":"1993","unstructured":"Spivey, J.: The Z notation: A Reference Manual, 2nd edn. Prentice-Hall, Englewood Cliffs (1993)","edition":"2"},{"key":"42_CR19","unstructured":"Sun microsystems. Java Card 2.1.1 Virtual Machine Specification (2000), \n\nhttp:\/\/java.sun.com\/products\/javacard\/javacard21.html#specification"},{"issue":"3","key":"42_CR20","first-page":"103","volume":"17","author":"J. Tretmans","year":"1996","unstructured":"Tretmans, J.: Test generation with inputs, outputs and repetitive quiescence. Software-Concepts and Tools\u00a017(3), 103\u2013120 (1996)","journal-title":"Software-Concepts and Tools"}],"container-title":["Lecture Notes in Computer Science","FME 2003: Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-45236-2_42","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,23]],"date-time":"2020-01-23T13:07:09Z","timestamp":1579784829000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-45236-2_42"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540408284","9783540452362"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-45236-2_42","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2003]]},"assertion":[{"value":"25 September 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}