{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,4]],"date-time":"2022-04-04T23:37:15Z","timestamp":1649115435139},"reference-count":24,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2009,3,20]],"date-time":"2009-03-20T00:00:00Z","timestamp":1237507200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2009,7]]},"DOI":"10.1007\/s10009-009-0108-3","type":"journal-article","created":{"date-parts":[[2009,3,19]],"date-time":"2009-03-19T01:53:07Z","timestamp":1237427587000},"page":"175-185","source":"Crossref","is-referenced-by-count":0,"title":["An automated testing experiment for layered embedded C code"],"prefix":"10.1007","volume":"11","author":[{"given":"Boutheina","family":"Chetali","sequence":"first","affiliation":[]},{"given":"Quang-Huy","family":"Nguyen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2009,3,20]]},"reference":[{"key":"108_CR1","unstructured":"Chen, Z.: Java Card Technology for Smart Cards: Architecture and Programmer\u2019s Guide. The Java Series. Addison-Wesley, Reading (2000)"},{"issue":"2\u20133","key":"108_CR2","doi-asserted-by":"crossref","first-page":"140","DOI":"10.1007\/s10009-003-0128-3","volume":"5","author":"A. Pretschner","year":"2004","unstructured":"Pretschner A., Slotosch O., Aiglstorfer E., Kriebel S.: Model based testing for real\u2014the inhouse card case study. J. Softw. Tools Technol. Transf. 5(2\u20133), 140\u2013157 (2004)","journal-title":"J. Softw. Tools Technol. Transf."},{"key":"108_CR3","volume-title":"Proof, Language and Interaction, Essays in Honour of Robin Milner","author":"G. Berry","year":"2000","unstructured":"Berry G.: The foundation of Esterel. In: Plotkin, G., Stirling, C., Tofte, M. (eds) Proof, Language and Interaction, Essays in Honour of Robin Milner., MIT press, Cambridge (2000)"},{"key":"108_CR4","unstructured":"Andr\u00e9, C.: Syncharts: a visual representation of reactive behaviors. Technical Report RR 95\u201352, rev. RR (96\u201356), I3S, Sophia-Antipolis, France, Rev. April (1996)"},{"issue":"7","key":"108_CR5","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"J.C. King","year":"1976","unstructured":"King J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385\u2013394 (1976)","journal-title":"Commun. ACM"},{"issue":"3","key":"108_CR6","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1109\/TSE.1976.233817","volume":"2","author":"L. Clarke","year":"1976","unstructured":"Clarke L.: A system to generate test data and symbolically execute programs. IEEE Trans. Softw. Eng. 2(3), 215\u2013222 (1976)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"108_CR7","unstructured":"International Organization for Standardization (ISO). ISO\/IEC9646: Information processing systems\u2014Open Systems Interconnection\u2014Conformance testing methodology and framework (1999)"},{"key":"108_CR8","doi-asserted-by":"crossref","unstructured":"El-Far, I.K., Whittaker, J.A.: Model-based software testing. In: Marciniak, J.J. (ed.) Encyclopedia of Software Engineering, pp. 825\u2013837. Wiley, New York (2001)","DOI":"10.1002\/0471028959.sof207"},{"issue":"10","key":"108_CR9","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. Int. J. Softw. Pract. Exp. 34(10), 915\u2013948 (2004)","journal-title":"Int. J. Softw. Pract. Exp."},{"key":"108_CR10","doi-asserted-by":"crossref","unstructured":"Bouquet, F., Legeard, B., Peureux, F., Torreborre, E.: Mastering Test Generation from Smart Card Software Formal Models. In: Proc. of CASSIS\u201904. Lecture Notes in Computer Science, vol. 3362, pp. 70\u201385. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-30569-9_4"},{"key":"108_CR11","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/S1571-0661(04)80817-X","volume":"80","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. Electr. Notes Theor. Comput. Sci. 80, 1\u201315 (2003)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"108_CR12","doi-asserted-by":"crossref","unstructured":"Clarke, D., J\u8c6fn, T., Rusu, V., Zinovieva, E.: Automated test and oracle generation for smart-card applications. In: Proc. of E-SMART\u201901. Lecture Notes in Computer Science, vol. 2140, pp. 58\u201370. Springer, Berlin (2001)","DOI":"10.1007\/3-540-45418-7_6"},{"issue":"4","key":"108_CR13","doi-asserted-by":"crossref","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 Comput. Surv. 29(4), 366\u2013427 (1997)","journal-title":"ACM Comput. Surv."},{"issue":"4","key":"108_CR14","doi-asserted-by":"crossref","first-page":"328","DOI":"10.1109\/TSE.2005.52","volume":"31","author":"D. Coppit","year":"2005","unstructured":"Coppit D., Yang J., Khurshid S., Le W., Sullivan K.J.: Software assurance by bounded exhaustive testing. IEEE Trans. Softw. Eng. 31(4), 328\u2013339 (2005)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"108_CR15","doi-asserted-by":"crossref","unstructured":"Bigot, C., Faivre, A., Gaston, C., Simon, J.: Automatic test generation on a (U)SIM smartcard. In: Domingo-Ferrer, J., Posegga, J., Schreckling, D. (eds.) Proc. of CARDIS\u201906. Lecture Notes in Computer Science, vol. 3928. Springer, Berlin (2006 to appear)","DOI":"10.1007\/11733447_25"},{"key":"108_CR16","doi-asserted-by":"crossref","unstructured":"Cheon, Y., Leavens, G.T.: A simple and practical approach to unit testing: the JML and JUnit way. In: Magnusson, B. (ed.) Proceedings of ECOOP\u201902. Lecture Notes in Computer Science, vol. 2374, pp. 231\u2013255. Springer, Berlin (2002)","DOI":"10.1007\/3-540-47993-7_10"},{"issue":"4","key":"108_CR17","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1145\/1013886.1007526","volume":"29","author":"W. Visser","year":"2004","unstructured":"Visser W., P\u0103s\u0103reanu C.S., Khurshid S.: Test input generation with Java PathFinder. SIGSOFT Softw. Eng. Notes 29(4), 97\u2013107 (2004)","journal-title":"SIGSOFT Softw. Eng. Notes"},{"key":"108_CR18","doi-asserted-by":"crossref","unstructured":"Barnett, M., Rustan, K., Leino, M., Schulte, W.: The Spec# programming system: an overview. In: Barthe, G., Burdy, L., Huisman, M. (eds.) Procs. of CASSIS\u201904. Lecture Notes in Computer Science, vol. 3362, pp. 49\u201369. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-30569-9_3"},{"key":"108_CR19","doi-asserted-by":"crossref","unstructured":"Campbell, C., Grieskamp, W., Nachmanson, L., Schulte, W., Tillmann, N., Veanes, M.: Testing concurrent object-oriented systems with Spec Explorer (extended abstract). In: Fitzgerald, J., Hayes, I.J., Tarlecki, A. (eds.) Proc. of FM\u201905. Lecture Notes in Computer Science, vol. 3582, pp. 542\u2013547. Springer, Berlin (2005)","DOI":"10.1007\/11526841_38"},{"key":"108_CR20","unstructured":"Common criteria for information technology security evaluation, August 1999. Version 2.1. http:\/\/www.commoncriteriaportal.org\/"},{"key":"108_CR21","doi-asserted-by":"crossref","unstructured":"Andronick, J., Chetali, B., Paulin-Mohring, C.: Formal verification of security properties of smart card embedded source code. In: Fitzgerald, J., Hayes, I.J., Tarlecki, A. (eds.) Proc. of FM\u201905. Lecture Notes in Computer Science, vol. 3582, pp. 302\u2013317. Springer, Berlin (2005)","DOI":"10.1007\/11526841_21"},{"key":"108_CR22","doi-asserted-by":"crossref","unstructured":"Andronick, J., Chetali, B., Ly, O.: Using Coq to verify Java Card Applet isolation properties. In: Basin, D.A., Wolff, B. (eds.) Proc. of TPHOLs\u201903. Lecture Notes in Computer Science, vol. 2758, pp. 335\u2013351. Springer, Berlin (2003)","DOI":"10.1007\/10930755_22"},{"key":"108_CR23","doi-asserted-by":"crossref","unstructured":"Nguyen, Q-H., Chetali, B.: Certifying Native Java Card API by formal refinement. In: Domingo-Ferrer, J., Posegga, J., Schreckling, D. (eds.) Proc. of CARDIS\u201906. Lecture Notes in Computer Science, vol. 3928, pp. 313\u2013328. Springer, Berlin (2006)","DOI":"10.1007\/11733447_23"},{"key":"108_CR24","doi-asserted-by":"crossref","unstructured":"Casset, L.: Development of an embedded verifier for Java Card byte code using formal methods. In: Eriksson, L.-H., Lindsay, P. (eds.) Proc. of FME\u201902. Lecture Notes in Computer Science, vol. 2391, pp. 290\u2013309 (2002)","DOI":"10.1007\/3-540-45614-7_17"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-009-0108-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-009-0108-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-009-0108-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T03:25:24Z","timestamp":1559100324000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-009-0108-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,3,20]]},"references-count":24,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2009,7]]}},"alternative-id":["108"],"URL":"https:\/\/doi.org\/10.1007\/s10009-009-0108-3","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,3,20]]}}}