{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,23]],"date-time":"2025-03-23T02:10:22Z","timestamp":1742695822892,"version":"3.40.2"},"reference-count":48,"publisher":"Wiley","issue":"6","license":[{"start":{"date-parts":[[2012,3,13]],"date-time":"2012-03-13T00:00:00Z","timestamp":1331596800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/onlinelibrary.wiley.com\/termsAndConditions#vor"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Software Testing Verif & Rel"],"published-print":{"date-parts":[[2012,9]]},"abstract":"SUMMARY<\/jats:title>This article presents a model\u2010based test generation technique, from user\u2010defined scenarios, for behavioral models expressed as B machines. Scenarios are expressed using a customized formalism, based on regular expressions, that makes it possible to describe sequences of operation calls possibly reaching specific states of the system. A symbolic animation engine, simulating the execution of a model using constraint logic programming, is then exploited to play the unfolded scenarios on the model and to instantiate the test cases, providing the expected results used to establish the conformance verdict. This approach is tool supported by a research prototype and has been successfully applied in an industrial context of a smart card applet. This tool is extended by a scenario generator, which automatically generates testing strategies for exercising user\u2010defined properties, written using specific patterns. Copyright \u00a9 2012 John Wiley & Sons, Ltd.<\/jats:p>","DOI":"10.1002\/stvr.1467","type":"journal-article","created":{"date-parts":[[2012,3,13]],"date-time":"2012-03-13T08:47:24Z","timestamp":1331628444000},"page":"407-434","source":"Crossref","is-referenced-by-count":2,"title":["Scenario\u2010based testing using symbolic animation of B\u2009models"],"prefix":"10.1002","volume":"22","author":[{"given":"Fr\u00e9d\u00e9ric","family":"Dadeau","sequence":"first","affiliation":[{"name":"FEMTO\u2010ST \u2013 UMR CNRS 6174\/INRIA CASSIS 16 route de Gray 25030 Besan\u00e7on France"}]},{"given":"Kalou Cabrera","family":"Castillos","sequence":"additional","affiliation":[{"name":"FEMTO\u2010ST \u2013 UMR CNRS 6174\/INRIA CASSIS 16 route de Gray 25030 Besan\u00e7on France"}]},{"given":"R\u00e9gis","family":"Tissot","sequence":"additional","affiliation":[{"name":"FEMTO\u2010ST \u2013 UMR CNRS 6174\/INRIA CASSIS 16 route de Gray 25030 Besan\u00e7on France"}]}],"member":"311","published-online":{"date-parts":[[2012,3,13]]},"reference":[{"volume-title":"Black\u2010box Testing: Techniques for Functional Testing of Software and Systems","year":"1995","author":"Beizer B","key":"e_1_2_12_2_1"},{"volume-title":"Practical Model\u2010based Testing \u2013 A Tools Approach","year":"2006","author":"Utting M","key":"e_1_2_12_3_1"},{"doi-asserted-by":"publisher","key":"e_1_2_12_4_1","DOI":"10.1007\/978-3-642-18216-7"},{"doi-asserted-by":"publisher","key":"e_1_2_12_5_1","DOI":"10.1017\/CBO9780511624162"},{"doi-asserted-by":"crossref","unstructured":"JaffuelE LegeardB.LEIRIOS test generator: automated test generation from B models.B'2007 the 7th int. B Conference \u2010 Industrial Tool Session volume 4355 ofLNCS Besancon France January2007;277\u2013280. Springer.","key":"e_1_2_12_6_1","DOI":"10.1007\/11955757_29"},{"doi-asserted-by":"publisher","key":"e_1_2_12_7_1","DOI":"10.1016\/j.entcs.2004.12.009"},{"doi-asserted-by":"publisher","key":"e_1_2_12_8_1","DOI":"10.1007\/978-3-540-45236-2_46"},{"doi-asserted-by":"publisher","key":"e_1_2_12_9_1","DOI":"10.1002\/stvr.300"},{"doi-asserted-by":"crossref","unstructured":"J\u00f6bstlE WeiglhoferM AichernigBK WotawaF.When BDDS fail: conformance testing with symbolic execution and SMT solving.Proceedings of the 2010 Third International Conference on Software Testing Verification and Validation ICST '10 Washington DC USA 2010;479\u2013488. IEEE Computer Society.","key":"e_1_2_12_10_1","DOI":"10.1109\/ICST.2010.48"},{"doi-asserted-by":"crossref","unstructured":"JulliandJ MassonP\u2010A TissotR.Generating security tests in addition to functional tests.Ast'08 3rd Int. Workshop on Automation of Software Test Leipzig Germany May2008;41\u201344. ACM Press.","key":"e_1_2_12_11_1","DOI":"10.1145\/1370042.1370051"},{"doi-asserted-by":"publisher","key":"e_1_2_12_12_1","DOI":"10.1007\/978-3-642-00982-2"},{"volume-title":"The Unified Modeling Language Reference Manual","year":"1999","author":"Rumbaugh J","key":"e_1_2_12_13_1"},{"doi-asserted-by":"publisher","key":"e_1_2_12_14_1","DOI":"10.1007\/978-1-4615-5229-1_12"},{"doi-asserted-by":"crossref","unstructured":"BehmP BenoitP FaivreA MeynadierJ\u2010M.M\u00e9t\u00e9or: a successful application of B in a large project Fm'99 \u2010Formal Methods \u2010volume 1 number 1708 inLNCS September1999;348\u2013387. Springer.","key":"e_1_2_12_15_1","DOI":"10.1007\/3-540-48119-2_22"},{"doi-asserted-by":"crossref","unstructured":"LanetJ\u2010L RequetA.Formal proof of smart card applets correctness Cardis '98: Proceedings of the International Conference on Smart Card Research and Applications London UK 2000;85\u201397. Springer\u2010Verlag.","key":"e_1_2_12_16_1","DOI":"10.1007\/10721064_7"},{"unstructured":"MarletR MetayerDL.2001.Security properties and Java Card specificities to be studied in the SecSafe project Technical Report SECSAFETL\u2010006 Trusted Logics.","key":"e_1_2_12_17_1"},{"doi-asserted-by":"crossref","unstructured":"BouquetF LegeardB.Reification of executable test scripts in formal specification\u2010based test generation: the Java Card transaction mechanism case study.Proc. of Fme'03 Formal Method Europe volume 2805 ofLNCS Pisa Italy September2003;778\u2013795.","key":"e_1_2_12_18_1","DOI":"10.1007\/978-3-540-45236-2_42"},{"unstructured":"Smart card standard: Part 4: interindustry commands for interchange.Technical Report ISO\/IEC 1995.","key":"e_1_2_12_19_1"},{"key":"e_1_2_12_20_1","series-title":"LNCS","first-page":"268","volume-title":"FME '93: First International Symposium of Formal Methods Europe","author":"Dick J","year":"1993"},{"doi-asserted-by":"publisher","key":"e_1_2_12_21_1","DOI":"10.1007\/s10009-003-0123-8"},{"unstructured":"AmbertF BouquetF CheminS GuenaudS LegeardB PeureuxF VaceletN UttingM.BZ\u2010TT: a tool\u2010set for test generation from Z and B using constraint logic programming.Proc. of Formal Approaches to Testing of Software FATES 2002 (workshop of concur'02) Brn\u00f6 R\u00e9publique Tch\u00e8que August2002105\u2013120. INRIA report.","key":"e_1_2_12_22_1"},{"doi-asserted-by":"publisher","key":"e_1_2_12_23_1","DOI":"10.1016\/0743-1066(94)90033-7"},{"volume-title":"Foundations of Constraint Satisfaction","year":"1993","author":"Tsang E","key":"e_1_2_12_24_1"},{"doi-asserted-by":"publisher","key":"e_1_2_12_25_1","DOI":"10.1002\/spe.597"},{"key":"e_1_2_12_26_1","series-title":"LNCS","volume-title":"Fundamental Approaches to Software Engineering, 7th Int. Conf., FASE 2004","author":"Ledru Y","year":"2004"},{"doi-asserted-by":"crossref","unstructured":"DwyerMB AvruninGS CorbettJC.Patterns in property specifications for finite\u2010state verification.Icse'99: Proceedings of the 21st international conference on software engineering Los Alamitos CA USA 1999;411\u2013420. IEEE Computer Society Press.","key":"e_1_2_12_27_1","DOI":"10.1145\/302405.302672"},{"doi-asserted-by":"publisher","key":"e_1_2_12_28_1","DOI":"10.1007\/11415787_18"},{"doi-asserted-by":"crossref","unstructured":"DadeauF de\u2009KermadecA TissotR.Combining scenario\u2010 and model\u2010based testing to ensure POSIX compliance.Abz'2008 International Conference on ASM B and Z volume5238ofLNCS London United Kingdom September2008;153\u2013166. Springer.","key":"e_1_2_12_29_1","DOI":"10.1007\/978-3-540-87603-8_13"},{"issue":"1","key":"e_1_2_12_30_1","first-page":"335","article-title":"An access control model based testing approach for smart card applications: results of the POSÉ project","volume":"5","author":"Masson P\u2010A","year":"2010","journal-title":"JIAS, Journal of Information Assurance and Security"},{"unstructured":"Common criteria for information technology security evaluation version 3.1.Technical Report CCMB\u20102006\u201009\u2010001 Sept2006.","key":"e_1_2_12_31_1"},{"doi-asserted-by":"crossref","unstructured":"WittevrongelJ MaurerF.SCENTOR: scenario\u2010based testing of e\u2010business applications.Wetice '01: Proceedings of the 10th IEEE International Workshops on Enabling Technologies Washington DC USA 2001;41\u201348. IEEE Computer Society.","key":"e_1_2_12_32_1","DOI":"10.1109\/ENABL.2001.953386"},{"unstructured":"RyserJ GlinzM.A practical approach to validating and testing software systems using scenarios.Quality Week Europe Brussels 1999.","key":"e_1_2_12_33_1"},{"key":"e_1_2_12_34_1","first-page":"288","article-title":"Scenario\u2010based object\u2010oriented test frameworks for testing distributed systems","volume":"0","author":"Tsai WT","year":"2003","journal-title":"Future Trends of Distributed Computing Systems, IEEE International Workshop"},{"volume-title":"Testing Object\u2010oriented Systems: Models, Patterns, and Tools","year":"1999","author":"Binder RV","key":"e_1_2_12_35_1"},{"doi-asserted-by":"crossref","unstructured":"AugustonM MichaelJB ShingM\u2010T.Environment behavior models for scenario generation and testing automation.A\u2010most '05: Proceedings of the 1st international workshop on advances in model\u2010based testing New York NY USA 2005;1\u20136. ACM.","key":"e_1_2_12_36_1","DOI":"10.1145\/1083274.1083284"},{"doi-asserted-by":"crossref","unstructured":"ClarkeD J\u00e9ronT RusuV ZinovievaE.STG: a tool for generating symbolic test programs and oracles from operational specifications.Esec\/fse\u20109: Proceedings of the 8th european software engineering conference held jointly with 9th ACM SIGSOFT international symposium on foundations of software engineering New York NY USA 2001;301\u2013302. ACM.","key":"e_1_2_12_37_1","DOI":"10.1145\/503209.503252"},{"unstructured":"MauryO LedruY du\u2009BousquetL.Int\u00e9gration de TOBIAS et UCASTING pour la g\u00e9n\u00e9ration de tests 16th International Conference Software and Systems and their applications\u2010ICSSEA 2003.","key":"e_1_2_12_38_1"},{"doi-asserted-by":"crossref","unstructured":"van AertryckL BenvenisteM Le\u2009M\u00e9tayerD.Casting: a formally based software test generation method.ICFEM '97: Proceedings of the 1st international conference on formal engineering methods Washington DC USA 1997;101. IEEE Computer Society.","key":"e_1_2_12_39_1","DOI":"10.1109\/ICFEM.1997.630411"},{"doi-asserted-by":"publisher","key":"e_1_2_12_40_1","DOI":"10.1145\/1095430.1081749"},{"unstructured":"The SpecExplorer 2010 web site 2010.http:\/\/msdn.microsoft.com\/en\u2010us\/devlabs\/ee692301.aspx.","key":"e_1_2_12_41_1"},{"doi-asserted-by":"publisher","key":"e_1_2_12_42_1","DOI":"10.1145\/318774.318939"},{"unstructured":"TanL SokolskyO LeeI.Specification\u2010based testing with linear temporal logic.Iri'2004 ieee int. conf. on information reuse and integration November2004;413\u2013498.","key":"e_1_2_12_43_1"},{"doi-asserted-by":"publisher","key":"e_1_2_12_44_1","DOI":"10.1007\/s11219-007-9031-6"},{"doi-asserted-by":"publisher","key":"e_1_2_12_45_1","DOI":"10.1145\/1291535.1291537"},{"doi-asserted-by":"publisher","key":"e_1_2_12_46_1","DOI":"10.1016\/j.entcs.2008.11.004"},{"doi-asserted-by":"publisher","key":"e_1_2_12_47_1","DOI":"10.1007\/11526841_14"},{"volume-title":"The Object Constraint Language Second Edition: Getting Your Models Ready for MDA","year":"2003","author":"Warmer J","key":"e_1_2_12_48_1"},{"key":"e_1_2_12_49_1","article-title":"The rodin formal modelling tool","author":"Butler M","year":"2007","journal-title":"BCS\u2010FACS Christmas 2007 Meeting \u2010 Formal Methods In Industry, London"}],"container-title":["Software Testing, Verification and Reliability"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.wiley.com\/onlinelibrary\/tdm\/v1\/articles\/10.1002%2Fstvr.1467","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/pdf\/10.1002\/stvr.1467","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,23]],"date-time":"2025-03-23T01:29:44Z","timestamp":1742693384000},"score":1,"resource":{"primary":{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/10.1002\/stvr.1467"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,3,13]]},"references-count":48,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2012,9]]}},"alternative-id":["10.1002\/stvr.1467"],"URL":"https:\/\/doi.org\/10.1002\/stvr.1467","archive":["Portico"],"relation":{},"ISSN":["0960-0833","1099-1689"],"issn-type":[{"type":"print","value":"0960-0833"},{"type":"electronic","value":"1099-1689"}],"subject":[],"published":{"date-parts":[[2012,3,13]]}}}