{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T18:04:42Z","timestamp":1725473082710},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540496991"},{"type":"electronic","value":"9783540497035"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11940197_15","type":"book-chapter","created":{"date-parts":[[2006,11,22]],"date-time":"2006-11-22T07:23:21Z","timestamp":1164180201000},"page":"225-239","source":"Crossref","is-referenced-by-count":7,"title":["Safety Property Driven Test Generation from JML Specifications"],"prefix":"10.1007","author":[{"given":"Fabrice","family":"Bouquet","sequence":"first","affiliation":[]},{"given":"Fr\u00e9d\u00e9ric","family":"Dadeau","sequence":"additional","affiliation":[]},{"given":"Julien","family":"Groslambert","sequence":"additional","affiliation":[]},{"given":"Jacques","family":"Julliand","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"15_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B Book","author":"J.-R. Abrial","year":"1996","unstructured":"Abrial, J.R.: The B Book. Cambridge University Press, Cambridge (1996)"},{"key":"15_CR2","first-page":"46","volume-title":"ICFEM 1998","author":"P. Ammann","year":"1998","unstructured":"Ammann, P., Black, P.E., Majurski, W.: Using model checking to generate tests from specifications. In: ICFEM 1998, pp. 46\u201355. IEEE Comp. Soc. Press, Los Alamitos (1998)"},{"key":"15_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1007\/11813040_29","volume-title":"FM 2006: Formal Methods","author":"F. Bouquet","year":"2006","unstructured":"Bouquet, F., Dadeau, F., Legeard, B.: Automated Boundary Test Generation from JML Specifications. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol.\u00a04085, pp. 428\u2013443. Springer, Heidelberg (2006)"},{"key":"15_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/11526841_7","volume-title":"FM 2005: Formal Methods","author":"F. Bouquet","year":"2005","unstructured":"Bouquet, F., Dadeau, F., Legeard, B., Utting, M.: Symbolic Animation of JML Specifications. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol.\u00a03582, pp. 75\u201390. Springer, Heidelberg (2005)"},{"key":"15_CR5","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1145\/566172.566191","volume-title":"ISSTA 2002","author":"C. Boyapati","year":"2002","unstructured":"Boyapati, C., Khurshid, S., Marinov, D.: Korat: automated testing based on java predicates. In: ISSTA 2002, pp. 123\u2013133. ACM Press, New York (2002)"},{"issue":"1-3","key":"15_CR6","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1016\/j.scico.2004.05.011","volume":"55","author":"C.-B. Breunesse","year":"2005","unstructured":"Breunesse, C.-B., Cata\u00f1o, N., Huisman, M., Jacobs, B.: Formal methods for smart cards: an experience report. Sci. Comput. Program.\u00a055(1-3), 53\u201380 (2005)","journal-title":"Sci. Comput. Program."},{"key":"15_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1007\/978-3-540-45236-2_24","volume-title":"FME 2003: Formal Methods","author":"L. Burdy","year":"2003","unstructured":"Burdy, L., Requet, A., Lanet, J.L.: Java Applet Correctness: a Developer-Oriented Approach. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805, pp. 422\u2013439. Springer, Heidelberg (2003)"},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: ICSE, pp. 411\u2013420 (1999)","DOI":"10.1145\/302405.302672"},{"key":"15_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1007\/11693017_27","volume-title":"Fundamental Approaches to Software Engineering","author":"A. Giorgetti","year":"2006","unstructured":"Giorgetti, A., Groslambert, J.: Jag: Jml annotation generation for verifying temporal properties. In: Baresi, L., Heckel, R. (eds.) FASE 2006. LNCS, vol.\u00a03922, pp. 373\u2013376. Springer, Heidelberg (2006)"},{"issue":"5","key":"15_CR10","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Trans. on Software Engineering\u00a023(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. on Software Engineering"},{"key":"15_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/978-3-540-39656-7_11","volume-title":"Formal Methods for Components and Objects","author":"G.T. Leavens","year":"2003","unstructured":"Leavens, G.T., Cheon, Y., Clifton, C., Ruby, C., Cok, D.R.: How the Design of JML Accomodates Both Runtime Assertion Checking and Formal Verification. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2002. LNCS, vol.\u00a02852, pp. 262\u2013284. Springer, Heidelberg (2003)"},{"key":"15_CR12","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/978-1-4615-5229-1_12","volume-title":"Behavioral Specifications of Businesses and Systems","author":"G.T. Leavens","year":"1999","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: JML: A notation for detailed design. In: Kilov, H., Rumpe, B., Simmonds, I. (eds.) Behavioral Specifications of Businesses and Systems, pp. 175\u2013188. Kluwer Academic Publishers, Boston (1999)"},{"key":"15_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/978-3-540-24721-0_21","volume-title":"Fundamental Approaches to Software Engineering","author":"Y. Ledru","year":"2004","unstructured":"Ledru, Y., du Bousquet, L., Maury, O., Bontron, P.: Filtering TOBIAS Combinatorial Test Suites. In: Wermelinger, M., Margaria-Steffen, T. (eds.) FASE 2004. LNCS, vol.\u00a02984, pp. 281\u2013294. Springer, Heidelberg (2004)"},{"key":"15_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-540-30569-9_3","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"K.R.M. Leino","year":"2005","unstructured":"Leino, K.R.M., Barnett, M., Schulte, W.: The Spec# Programming System: An Overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 49\u201369. Springer, Heidelberg (2005)"},{"key":"15_CR15","unstructured":"Marlet, R., Mesnil, C.: Demoney: A demonstrative electronic purse - card specification. Technical report, Trusted Logic (2002)"},{"key":"15_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1007\/11558569_18","volume-title":"Quality of Software Architectures and Software Quality","author":"C. Oriat","year":"2005","unstructured":"Oriat, C.: Jartege: A tool for random generation of unit tests for java classes. In: Reussner, R., Mayer, J., Stafford, J.A., Overhage, S., Becker, S., Schroeder, P.J. (eds.) QoSA 2005 and SOQUA 2005. LNCS, vol.\u00a03712, pp. 242\u2013256. Springer, Heidelberg (2005)"},{"key":"15_CR17","unstructured":"Sun microsystems. Java Card 2.1.1 Virtual Machine Specification (May 2000), \n \n http:\/\/java.sun.com\/products\/javacard\/javacard21.html#specification"},{"key":"15_CR18","unstructured":"Tan, L., Sokolsky, O., Lee, I.: Specification-based testing with linear temporal logic. In: IRI, pp. 493\u2013498. IEEE Systems, Man, and Cybernetics Society (2004)"},{"key":"15_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/3-540-45719-4_23","volume-title":"Algebraic Methodology and Software Technology","author":"K. Trentelman","year":"2002","unstructured":"Trentelman, K., Huisman, M.: Extending JML Specifications with Temporal Logic. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol.\u00a02422, pp. 334\u2013348. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Formal Approaches to Software Testing and Runtime Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11940197_15.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:50:16Z","timestamp":1619509816000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11940197_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540496991","9783540497035"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/11940197_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}