{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T15:16:41Z","timestamp":1781104601165,"version":"3.54.1"},"reference-count":271,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2009,2,1]],"date-time":"2009-02-01T00:00:00Z","timestamp":1233446400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["GR\/R43150"],"award-info":[{"award-number":["GR\/R43150"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Comput. Surv."],"published-print":{"date-parts":[[2009,2]]},"abstract":"<jats:p>Formal methods and testing are two important approaches that assist in the development of high-quality software. While traditionally these approaches have been seen as rivals, in recent years a new consensus has developed in which they are seen as complementary. This article reviews the state of the art regarding ways in which the presence of a formal specification can be used to assist testing.<\/jats:p>","DOI":"10.1145\/1459352.1459354","type":"journal-article","created":{"date-parts":[[2009,2,25]],"date-time":"2009-02-25T14:44:30Z","timestamp":1235573070000},"page":"1-76","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":267,"title":["Using formal specifications to support testing"],"prefix":"10.1145","volume":"41","author":[{"given":"Robert M.","family":"Hierons","sequence":"first","affiliation":[{"name":"Brunel University, Middlesex, U.K."}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kirill","family":"Bogdanov","sequence":"additional","affiliation":[{"name":"University of Sheffield, Sheffield, U.K."}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jonathan P.","family":"Bowen","sequence":"additional","affiliation":[{"name":"King's College London, London, U.K."}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rance","family":"Cleaveland","sequence":"additional","affiliation":[{"name":"University of Maryland, College Park, MD"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"John","family":"Derrick","sequence":"additional","affiliation":[{"name":"University of Sheffield, Sheffield, U.K."}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jeremy","family":"Dick","sequence":"additional","affiliation":[{"name":"integrate systems engineering ltd., Bath, U.K."}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marian","family":"Gheorghe","sequence":"additional","affiliation":[{"name":"University of Sheffield, Sheffield, U.K."}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mark","family":"Harman","sequence":"additional","affiliation":[{"name":"King's College London, London, U.K."}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kalpesh","family":"Kapoor","sequence":"additional","affiliation":[{"name":"Indian Institute of Technology Guwahati, Guwahati, India"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Paul","family":"Krause","sequence":"additional","affiliation":[{"name":"University of Surrey, Surrey, U.K."}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Gerald","family":"L\u00fcttgen","sequence":"additional","affiliation":[{"name":"University of York, York, U.K."}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Anthony J. H.","family":"Simons","sequence":"additional","affiliation":[{"name":"University of Sheffield, Sheffield, U.K."}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sergiy","family":"Vilkomir","sequence":"additional","affiliation":[{"name":"University of Tennessee, Greenville, NC"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Martin R.","family":"Woodward","sequence":"additional","affiliation":[{"name":"(Deceased)"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Hussein","family":"Zedan","sequence":"additional","affiliation":[{"name":"De Montfort University, Leicester, U.K."}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2009,2,23]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"The B-Book: Assigning Programs to Meanings","author":"Abrial J.-R.","unstructured":"Abrial , J.-R. 1996. The B-Book: Assigning Programs to Meanings . Cambridge University Press , Cambridge, U.K. Abrial, J.-R. 1996. The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge, U.K."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/523981.852145"},{"key":"e_1_2_1_3_1","unstructured":"Aho A. V. Dahbura A. T. Lee D. and Uyar M. U. 1988. An optimization technique for protocol conformance test generation based on UIO sequences and Rural Chinese Postman Tours. In Protocol Specification Testing and Verification VIII. Elsevier (North-Holland) Amsterdam The Netherlands 75--86.  Aho A. V. Dahbura A. T. Lee D. and Uyar M. U. 1988. An optimization technique for protocol conformance test generation based on UIO sequences and Rural Chinese Postman Tours. In Protocol Specification Testing and Verification VIII. Elsevier (North-Holland) Amsterdam The Netherlands 75--86."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/647397.724691"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/HASE.2000.895462"},{"key":"e_1_2_1_7_1","volume-title":"Formal Methods Europe (FME","author":"Aichernig B. K.","year":"2001","unstructured":"Aichernig , B. K. 2001b. Test-case calculation through abstraction . In Formal Methods Europe (FME 2001 ), J. N. Oliveira and P. Zave, Eds . Lecture Notes in Computer Science, vol. 2021 . Springer-Verlag , Berlin, Germany, 571--589. Aichernig, B. K. 2001b. Test-case calculation through abstraction. In Formal Methods Europe (FME 2001), J. N. Oliveira and P. Zave, Eds. Lecture Notes in Computer Science, vol. 2021. Springer-Verlag, Berlin, Germany, 571--589."},{"key":"e_1_2_1_8_1","volume-title":"Proceedings of the 20th International Conference on Information Systems. 400--404","author":"Al-Amayreh A.","unstructured":"Al-Amayreh , A. and Zin , A. M . 1999. PROBE: A formal specification-based testing system . In Proceedings of the 20th International Conference on Information Systems. 400--404 . Al-Amayreh, A. and Zin, A. M. 1999. PROBE: A formal specification-based testing system. In Proceedings of the 20th International Conference on Information Systems. 400--404."},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of the 3rd International Conference on Achieving Quality in Software. Chapman and Hall","author":"Allen S. P.","unstructured":"Allen , S. P. and Woodward , M. R . 1996. Assessing the quality of specification-based testing . In Proceedings of the 3rd International Conference on Achieving Quality in Software. Chapman and Hall , London, U.K., 341--354. Allen, S. P. and Woodward, M. R. 1996. Assessing the quality of specification-based testing. In Proceedings of the 3rd International Conference on Achieving Quality in Software. Chapman and Hall, London, U.K., 341--354."},{"key":"e_1_2_1_10_1","volume-title":"Hybrid Automata: An Algorithmic approach to the specification and analysis of hybrid systems","author":"Alur R.","year":"1993","unstructured":"Alur , R. , Courcoubetis , C. , Henzinger , T. , and Ho , P . 1993 . Hybrid Automata: An Algorithmic approach to the specification and analysis of hybrid systems . In Hybrid Systems, R. L. Grossman, A. Nerode, A. P. Ravn, and H. Rischel, Eds. Lecture Notes in Computer Science , vol. 736 , 209--229. Alur, R., Courcoubetis, C., Henzinger, T., and Ho, P. 1993. Hybrid Automata: An Algorithmic approach to the specification and analysis of hybrid systems. In Hybrid Systems, R. L. Grossman, A. Nerode, A. P. Ravn, and H. Rischel, Eds. Lecture Notes in Computer Science, vol. 736, 209--229."},{"key":"e_1_2_1_11_1","volume-title":"17th International Colloquium, ICALP90","volume":"443","author":"Alur R.","unstructured":"Alur , R. and Dill , D . 1990. Automata for modeling real-time systems. In Automata, Languages and Programming , 17th International Colloquium, ICALP90 . Lecture Notes in Computer Science , vol. 443 . Springer-Verlag, Berlin, Germany, 322--335. Alur, R. and Dill, D. 1990. Automata for modeling real-time systems. In Automata, Languages and Programming, 17th International Colloquium, ICALP90. Lecture Notes in Computer Science, vol. 443. Springer-Verlag, Berlin, Germany, 322--335."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_2_1_13_1","volume-title":"Third International Workshop (HSCC). 6--19","author":"Alur R.","unstructured":"Alur , R. , Grosu , R. , Hur , Y. , Kumar , V. , and Lee , I . 2000. Modular specification of hybrid systems in CHARON. In Hybrid Systems: Computation and Control , Third International Workshop (HSCC). 6--19 . Alur, R., Grosu, R., Hur, Y., Kumar, V., and Lee, I. 2000. Modular specification of hybrid systems in CHARON. In Hybrid Systems: Computation and Control, Third International Workshop (HSCC). 6--19."},{"key":"e_1_2_1_14_1","volume-title":"Proceedings of the DIMACS\/SYCON Workshop, October 22--25","volume":"1066","author":"Alur R.","year":"1995","unstructured":"Alur , R. and Kurshan , R . 1996. Timing analysis in COSPAN. In Hybrid Systems III: Verification and Control , Proceedings of the DIMACS\/SYCON Workshop, October 22--25 , 1995 , Rutgers University, New Brunswick, NJ, USA, R. Alur, T. A. Henziger, and E. D. Sontag, Eds. Lecture Notes in Computer Science , vol. 1066 , 220--231. Alur, R. and Kurshan, R. 1996. Timing analysis in COSPAN. In Hybrid Systems III: Verification and Control, Proceedings of the DIMACS\/SYCON Workshop, October 22--25, 1995, Rutgers University, New Brunswick, NJ, USA, R. Alur, T. A. Henziger, and E. D. Sontag, Eds. Lecture Notes in Computer Science, vol. 1066, 220--231."},{"key":"e_1_2_1_15_1","unstructured":"Ambert F. Bouquet F. Chemin S. Guenaud S. Legeard B. Peureux F. Utting M. and Vacelet N. 2002. BZ-testing-tools: A tool-set for test generation from Z and B using constraint logic programming. In Formal Approaches to Testing Software (FATES 2002). INRIA Brno Czech Republic 105--120.  Ambert F. Bouquet F. Chemin S. Guenaud S. Legeard B. Peureux F. Utting M. and Vacelet N. 2002. BZ-testing-tools: A tool-set for test generation from Z and B using constraint logic programming. In Formal Approaches to Testing Software (FATES 2002). INRIA Brno Czech Republic 105--120."},{"key":"e_1_2_1_16_1","volume-title":"COMPASS '92, Proceedings of the 7th Annual Conference on Computer Assurance","author":"Amla N.","unstructured":"Amla , N. and Ammann , P . 1992. Using Z specifications in category partition testing . In COMPASS '92, Proceedings of the 7th Annual Conference on Computer Assurance ( Gaithersburg, MD). 15--18. Amla, N. and Ammann, P. 1992. Using Z specifications in category partition testing. In COMPASS '92, Proceedings of the 7th Annual Conference on Computer Assurance (Gaithersburg, MD). 15--18."},{"key":"e_1_2_1_17_1","volume-title":"Proceedings of the 2nd IEEE International Conference on Formal Engineering Methods (ICFEM","author":"Ammann P.","unstructured":"Ammann , P. , Black , P. E. , and Majurski , W . 1998. Using model checking to generate tests from specifications . In Proceedings of the 2nd IEEE International Conference on Formal Engineering Methods (ICFEM , Brisbane, Australia). 46--54. Ammann, P., Black, P. E., and Majurski, W. 1998. Using model checking to generate tests from specifications. In Proceedings of the 2nd IEEE International Conference on Formal Engineering Methods (ICFEM, Brisbane, Australia). 46--54."},{"key":"e_1_2_1_18_1","volume-title":"Proceedings of the 9th Annual Conference on Computer Assurance (COMPASS","author":"Ammann P.","unstructured":"Ammann , P. and Offutt , J . 1994. Using formal methods to derive test frames in category-partition testing . In Proceedings of the 9th Annual Conference on Computer Assurance (COMPASS , Gaithersburg, MD). 69--80. Ammann, P. and Offutt, J. 1994. Using formal methods to derive test frames in category-partition testing. In Proceedings of the 9th Annual Conference on Computer Assurance (COMPASS, Gaithersburg, MD). 69--80."},{"key":"e_1_2_1_19_1","volume-title":"Proceedings of the International Workshop on Automated Program Analysis, Testing and Verification","author":"Ammann P. E.","unstructured":"Ammann , P. E. and Black , P. E . 2000. Test generation and recognition with formal methods . In Proceedings of the International Workshop on Automated Program Analysis, Testing and Verification ( Limerick, Ireland). 64--67. Ammann, P. E. and Black, P. E. 2000. Test generation and recognition with formal methods. In Proceedings of the International Workshop on Automated Program Analysis, Testing and Verification (Limerick, Ireland). 64--67."},{"key":"e_1_2_1_20_1","volume-title":"Eds","author":"Antsaklis P.","year":"1995","unstructured":"Antsaklis , P. , Kohn , W. , Nerode , A. , and Sastry , S. , Eds . 1995 . Hybrid Systems II. Lecture Notes in Computer Science, vol. 999 . Springer-Verlag . Antsaklis, P., Kohn, W., Nerode, A., and Sastry, S., Eds. 1995. Hybrid Systems II. Lecture Notes in Computer Science, vol. 999. Springer-Verlag."},{"key":"e_1_2_1_21_1","series-title":"Lecture Notes in Computer Science","volume-title":"1997. Hybrid Systems IV","author":"Antsaklis P. J.","unstructured":"Antsaklis , P. J. , Ed. 1997. Hybrid Systems IV . Lecture Notes in Computer Science , vol. 1237 . Springer-Verlag, Berlin , Germany . Antsaklis, P. J., Ed. 1997. Hybrid Systems IV. Lecture Notes in Computer Science, vol. 1237. Springer-Verlag, Berlin, Germany."},{"key":"e_1_2_1_22_1","volume-title":"Hybrid Systems. Lecture Notes in Computer Science","volume":"1567","author":"Antsaklis P. J.","unstructured":"Antsaklis , P. J. , Kohn , W. , Lemmon , M. , Nerode , A. , and Sastry , S . 1999 . Hybrid Systems. Lecture Notes in Computer Science , vol. 1567 . Springer-Verlag. Antsaklis, P. J., Kohn, W., Lemmon, M., Nerode, A., and Sastry, S. 1999. Hybrid Systems. Lecture Notes in Computer Science, vol. 1567. Springer-Verlag."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.11.007"},{"key":"e_1_2_1_25_1","first-page":"494","article-title":"Communicating stream X-machines systems are no more than X-machines","volume":"5","author":"Balanescu T.","year":"1999","unstructured":"Balanescu , T. , Cowling , T. , Georgescu , H. , Gheorghe , M. , Holcombe , M. , and Vertan , C. 1999 . Communicating stream X-machines systems are no more than X-machines . J. Univers. Comput. Sci. 5 , 494 -- 507 . Balanescu, T., Cowling, T., Georgescu, H., Gheorghe, M., Holcombe, M., and Vertan, C. 1999. Communicating stream X-machines systems are no more than X-machines. J. Univers. Comput. Sci. 5, 494--507.","journal-title":"J. Univers. Comput. Sci."},{"key":"e_1_2_1_26_1","volume-title":"SPIN","volume":"2057","author":"Ball T.","year":"2001","unstructured":"Ball , T. and Rajamani , S . 2001. Automatically validating temporal safety properties of interfaces . In SPIN 2001 . Lecture Notes in Computer Science , vol. 2057 . Springer-Verlag, Berlin, Germany, 103--122. Ball, T. and Rajamani, S. 2001. Automatically validating temporal safety properties of interfaces. In SPIN 2001. Lecture Notes in Computer Science, vol. 2057. Springer-Verlag, Berlin, Germany, 103--122."},{"key":"e_1_2_1_27_1","volume-title":"Lecture Notes in Computer Science","volume":"2931","author":"Barnett M.","unstructured":"Barnett , M. , Grieskamp , W. , Nachmanson , L. , Schulte , W. , Tillmann , N. , and Veanes , M . 2003. Towards a tool environment for model--based testing with ASML. In Formal Approaches to Testing . Lecture Notes in Computer Science , vol. 2931 . Springer-Verlag, Berlin, Germany, 252--266. Barnett, M., Grieskamp, W., Nachmanson, L., Schulte, W., Tillmann, N., and Veanes, M. 2003. Towards a tool environment for model--based testing with ASML. In Formal Approaches to Testing. Lecture Notes in Computer Science, vol. 2931. Springer-Verlag, Berlin, Germany, 252--266."},{"key":"e_1_2_1_28_1","volume-title":"Proceedings of the World Congress on Formal Methods. 509--529","author":"Behnia S.","unstructured":"Behnia , S. and Waeselynck , H . 1999. Test criteria definition for B models . In Proceedings of the World Congress on Formal Methods. 509--529 . Behnia, S. and Waeselynck, H. 1999. Test criteria definition for B models. In Proceedings of the World Congress on Formal Methods. 509--529."},{"key":"e_1_2_1_29_1","volume-title":"Proceedings of the DIMACS\/SYCON Workshop, October 22--25","volume":"1066","author":"Bengtsson J.","year":"1995","unstructured":"Bengtsson , J. , Larsen , K. G. , Larson , F. , Pettersson , P. , and Yi , W . 1995. UppAal: A tool suite for automatic verification of real-time systems. In Hybrid Systems III: Verification and Control , Proceedings of the DIMACS\/SYCON Workshop, October 22--25 , 1995 , Rutgers University, New Brunswick, NJ, USA, R. Alur, T. A. Henzinger, and E. D. Sontag, Eds. Lecture Notes in Computer Science , vol. 1066 . Springer, Berlin, Germany, 232--243. Bengtsson, J., Larsen, K. G., Larson, F., Pettersson, P., and Yi, W. 1995. UppAal: A tool suite for automatic verification of real-time systems. In Hybrid Systems III: Verification and Control, Proceedings of the DIMACS\/SYCON Workshop, October 22--25, 1995, Rutgers University, New Brunswick, NJ, USA, R. Alur, T. A. Henzinger, and E. D. Sontag, Eds. Lecture Notes in Computer Science, vol. 1066. Springer, Berlin, Germany, 232--243."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/309847.310108"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1049\/sej.1991.0040"},{"key":"e_1_2_1_32_1","volume-title":"Proceedings of the ICSE","author":"Beyer D.","year":"2004","unstructured":"Beyer , D. , Chlipala , A. , Henzinger , T. , Jhala , R. , and Majumdar , R . 2004. Generating tests from counterexamples . In Proceedings of the ICSE 2004 . IEEE Computer Society Press, Los Alamitos, CA, 326--335. Beyer, D., Chlipala, A., Henzinger, T., Jhala, R., and Majumdar, R. 2004. Generating tests from counterexamples. In Proceedings of the ICSE 2004. IEEE Computer Society Press, Los Alamitos, CA, 326--335."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(96)00029-9"},{"key":"e_1_2_1_34_1","volume-title":"Lecture Notes in Computer Science","volume":"2900","author":"Bidoit M.","unstructured":"Bidoit , M. and Mosses , P . 2003. CASL User Manual: Introduction to Using the Common Algebraic Specification Language . Lecture Notes in Computer Science , vol. 2900 . Springer-Verlag, Berlin, Germany. Bidoit, M. and Mosses, P. 2003. CASL User Manual: Introduction to Using the Common Algebraic Specification Language. Lecture Notes in Computer Science, vol. 2900. Springer-Verlag, Berlin, Germany."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/0164-1212(86)90004-X"},{"key":"e_1_2_1_37_1","volume-title":"Proceedings of the 26th IEEE Computer Software and Applications (COMPSAC). 91--101","author":"Bowen J. P.","unstructured":"Bowen , J. P. , Bogdanov , K. , Clark , J. , Harman , M. , Hierons , R. M. , and Krause , P . 2002. FORTEST: Formal methods and testing . In Proceedings of the 26th IEEE Computer Software and Applications (COMPSAC). 91--101 . Bowen, J. P., Bogdanov, K., Clark, J., Harman, M., Hierons, R. M., and Krause, P. 2002. FORTEST: Formal methods and testing. In Proceedings of the 26th IEEE Computer Software and Applications (COMPSAC). 91--101."},{"key":"e_1_2_1_38_1","doi-asserted-by":"crossref","unstructured":"Bradfield J. and Stirling C. 2001. Modal logics and mu-calculi: An introduction. In Handbook of Process Algebra. Elsevier Science Amsterdam The Netherlands 293--330.  Bradfield J. and Stirling C. 2001. Modal logics and mu-calculi: An introduction. In Handbook of Process Algebra. Elsevier Science Amsterdam The Netherlands 293--330.","DOI":"10.1016\/B978-044482830-9\/50022-9"},{"key":"e_1_2_1_39_1","volume-title":"Protocol Specification, Testing, and Verification VIII. North-Holland","author":"Brinksma E.","unstructured":"Brinksma , E. 1988. A theory for the derivation of tests . In Protocol Specification, Testing, and Verification VIII. North-Holland , Amsterdam, The Netherlands , 63--74. Brinksma, E. 1988. A theory for the derivation of tests. In Protocol Specification, Testing, and Verification VIII. North-Holland, Amsterdam, The Netherlands, 63--74."},{"key":"e_1_2_1_40_1","doi-asserted-by":"crossref","unstructured":"Brinksma E. Heerink L. and Tretmans J. 1997. Developments in testing transition systems. In IFIP TC6 10th International Workshop on Testing of Communicating Systems. Kluwer Dordrecht The Netherlands 143--166.  Brinksma E. Heerink L. and Tretmans J. 1997. Developments in testing transition systems. In IFIP TC6 10th International Workshop on Testing of Communicating Systems. Kluwer Dordrecht The Netherlands 143--166.","DOI":"10.1007\/978-0-387-35198-8_10"},{"key":"e_1_2_1_41_1","doi-asserted-by":"crossref","unstructured":"Brinksma E. Heerink L. and Tretmans J. 1998. Factorized test generation for multi-input\/output transition systems. In IFIP TC6 11th International Workshop on Testing of Communicating Systems. Kluwer Dordrecht The Netherlands 67--82.   Brinksma E. Heerink L. and Tretmans J. 1998. Factorized test generation for multi-input\/output transition systems. In IFIP TC6 11th International Workshop on Testing of Communicating Systems. Kluwer Dordrecht The Netherlands 67--82.","DOI":"10.1007\/978-0-387-35381-4_5"},{"key":"e_1_2_1_42_1","unstructured":"Broekman B. and Notenboom E. 2003. Testing Embedded Software. Addison--Wesley London U.K.   Broekman B. and Notenboom E. 2003. Testing Embedded Software. Addison--Wesley London U.K."},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_2_1_45_1","volume-title":"SPIN '96","author":"Callahan J.","unstructured":"Callahan , J. , Schneider , F. , and Easterbrook , S . 1996. Automated software testing using model-checking . In SPIN '96 . Rutgers University, Brunswick, NJ, 118--127. Callahan, J., Schneider, F., and Easterbrook, S. 1996. Automated software testing using model-checking. In SPIN '96. Rutgers University, Brunswick, NJ, 118--127."},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/s001650070009"},{"key":"e_1_2_1_47_1","volume-title":"Z User Workshop, Cambridge 1994, J. P. Bowen and J. A. Hall, Eds. Workshops in Computing. Springer-Verlag","author":"Carrington D. A.","unstructured":"Carrington , D. A. and Stocks , P. A . 1994. A tale of two paradigms: Formal methods and software testing . In Z User Workshop, Cambridge 1994, J. P. Bowen and J. A. Hall, Eds. Workshops in Computing. Springer-Verlag , Berlin, Germany, 51--68. Carrington, D. A. and Stocks, P. A. 1994. A tale of two paradigms: Formal methods and software testing. In Z User Workshop, Cambridge 1994, J. P. Bowen and J. A. Hall, Eds. Workshops in Computing. Springer-Verlag, Berlin, Germany, 51--68."},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1016\/0169-7552(95)00125-5"},{"key":"e_1_2_1_49_1","volume-title":"Proceedings of the Conference on Formal Methods for Protocol Engineering and Distributed Systems (FORTE XII). 41--56","author":"Cavalli A. R.","unstructured":"Cavalli , A. R. , Lee , D. , Rinderknecht , C. , and Za\u00efdi , F . 1999. Hit-or-Jump: An algorithm for embedded testing with applications to in services . In Proceedings of the Conference on Formal Methods for Protocol Engineering and Distributed Systems (FORTE XII). 41--56 . Cavalli, A. R., Lee, D., Rinderknecht, C., and Za\u00efdi, F. 1999. Hit-or-Jump: An algorithm for embedded testing with applications to in services. In Proceedings of the Conference on Formal Methods for Protocol Engineering and Distributed Systems (FORTE XII). 41--56."},{"key":"e_1_2_1_50_1","volume-title":"Proceedings of the IFIP WG6.1 Ninth International Symposium on Protocol Specification, Testing and Verification. 119--130","author":"Chan W. Y. L.","unstructured":"Chan , W. Y. L. , Vuong , S. T. , and Ito , M. R . 1989. On test sequence generation for protocols . In Proceedings of the IFIP WG6.1 Ninth International Symposium on Protocol Specification, Testing and Verification. 119--130 . Chan, W. Y. L., Vuong, S. T., and Ito, M. R. 1989. On test sequence generation for protocols. In Proceedings of the IFIP WG6.1 Ninth International Symposium on Protocol Specification, Testing and Verification. 119--130."},{"key":"e_1_2_1_51_1","volume-title":"Proceedings of the 4th Irvine Software Symposium","author":"Chang J.","unstructured":"Chang , J. and Richardson , D . 1994. Static and dynamic specification slicing . In Proceedings of the 4th Irvine Software Symposium ( Irvine, CA). Chang, J. and Richardson, D. 1994. Static and dynamic specification slicing. In Proceedings of the 4th Irvine Software Symposium (Irvine, CA)."},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/287000.287004"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/366378.366380"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0950-5849(00)00112-9"},{"key":"e_1_2_1_55_1","volume-title":"Proceedings of the Workshop on Software Testing. IEEE Computer Society Press","author":"Choquet N.","year":"1986","unstructured":"Choquet , N. 1986 . Test data generation using a prolog with constraints . In Proceedings of the Workshop on Software Testing. IEEE Computer Society Press , Los Alamitos, CA, 132--141. Choquet, N. 1986. Test data generation using a prolog with constraints. In Proceedings of the Workshop on Software Testing. IEEE Computer Society Press, Los Alamitos, CA, 132--141."},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1978.231496"},{"key":"e_1_2_1_57_1","volume-title":"Proceedings of the 8th International Conference on Software Engineering and Knowledge Engineering (SEKE","author":"Ciancarini P.","unstructured":"Ciancarini , P. , Cimato , S. , and Mascolo , C . 1996. Engineering formal requirements: Analysis and testing . In Proceedings of the 8th International Conference on Software Engineering and Knowledge Engineering (SEKE , Lake Tahoe, CA). 385--392. Ciancarini, P., Cimato, S., and Mascolo, C. 1996. Engineering formal requirements: Analysis and testing. In Proceedings of the 8th International Conference on Software Engineering and Knowledge Engineering (SEKE, Lake Tahoe, CA). 385--392."},{"key":"e_1_2_1_58_1","volume-title":"CAV '99","volume":"1464","author":"Cimatti A.","unstructured":"Cimatti , A. , Clarke , E. M. , Giunchiglia , F. , and Roveri , M . 1999. NuSMV: A new symbolic model verifier . In CAV '99 . Lecture Notes in Computer Science , vol. 1464 . Springer-Verlag, Berlin, Germany, 495--499. Cimatti, A., Clarke, E. M., Giunchiglia, F., and Roveri, M. 1999. NuSMV: A new symbolic model verifier. In CAV '99. Lecture Notes in Computer Science, vol. 1464. Springer-Verlag, Berlin, Germany, 495--499."},{"key":"e_1_2_1_59_1","volume-title":"Workshop on Logics of Programs. Lecture Notes in Computer Science","volume":"131","author":"Clarke E. M.","unstructured":"Clarke , E. M. and Emerson , E. A . 1981. Synthesis of synchronization skeletons for branching time temporal logic . In Workshop on Logics of Programs. Lecture Notes in Computer Science , vol. 131 . Springer-Verlag, Berlin, Germany, 52--71. Clarke, E. M. and Emerson, E. A. 1981. Synthesis of synchronization skeletons for branching time temporal logic. In Workshop on Logics of Programs. Lecture Notes in Computer Science, vol. 131. Springer-Verlag, Berlin, Germany, 52--71."},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"e_1_2_1_61_1","unstructured":"Clarke E. M. Grumberg O. and Peled D. 1999. Model Checking. MIT Press Cambridge MA.   Clarke E. M. Grumberg O. and Peled D. 1999. Model Checking. MIT Press Cambridge MA."},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/242223.242257"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1982.235572"},{"key":"e_1_2_1_64_1","unstructured":"Cleaveland R. Li T. and Sims S. 2000. The Concurrency Workbench of the New Century. SUNY Stony Brook NY.  Cleaveland R. Li T. and Sims S. 2000. The Concurrency Workbench of the New Century. SUNY Stony Brook NY."},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/337180.337234"},{"key":"e_1_2_1_66_1","volume-title":"Proceedings of the 1st European Conference on Model-Driven Software Engineering. 106--117","author":"Craggs I.","unstructured":"Craggs , I. , Sardis , M. , and Heuillard , T . 2003. AGEDIS case studies: Model-based testing in industry . In Proceedings of the 1st European Conference on Model-Driven Software Engineering. 106--117 . Craggs, I., Sardis, M., and Heuillard, T. 2003. AGEDIS case studies: Model-based testing in industry. In Proceedings of the 1st European Conference on Model-Driven Software Engineering. 106--117."},{"key":"e_1_2_1_67_1","volume-title":"Z User Workshop, London 1992, J. P. Bowen and J. E. Nicholls, Eds. Workshops in Computing. Springer-Verlag","author":"Cusack E.","unstructured":"Cusack , E. and Wezeman , C . 1993. Deriving tests for objects specified in z . In Z User Workshop, London 1992, J. P. Bowen and J. E. Nicholls, Eds. Workshops in Computing. Springer-Verlag , Berlin, Germany, 180--195. Cusack, E. and Wezeman, C. 1993. Deriving tests for objects specified in z. In Z User Workshop, London 1992, J. P. Bowen and J. E. Nicholls, Eds. Workshops in Computing. Springer-Verlag, Berlin, Germany, 180--195."},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1016\/0164-1212(93)90025-S"},{"key":"e_1_2_1_69_1","volume-title":"Hybrid Systems. Lecture Notes in Computer Science","volume":"1066","author":"Daws C.","unstructured":"Daws , C. , Olivero , A. , Tripakis , S. , and Yovine , S . 1995. The tool kronos . In Hybrid Systems. Lecture Notes in Computer Science , vol. 1066 . Springer, Berlin, Germany, 208--219. Daws, C., Olivero, A., Tripakis, S., and Yovine, S. 1995. The tool kronos. In Hybrid Systems. Lecture Notes in Computer Science, vol. 1066. Springer, Berlin, Germany, 208--219."},{"key":"e_1_2_1_70_1","first-page":"4","article-title":"On-the-fly conformance testing using Spin","volume":"2","author":"de Vries R. G.","year":"2000","unstructured":"de Vries , R. G. and Tretmans , J. 2000 . On-the-fly conformance testing using Spin . Softw. Tools Technol. Transf. 2 , 4 (Mar.), 382--393. de Vries, R. G. and Tretmans, J. 2000. On-the-fly conformance testing using Spin. Softw. Tools Technol. Transf. 2, 4 (Mar.), 382--393.","journal-title":"Softw. Tools Technol. Transf."},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/359104.359106"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1002\/(SICI)1099-1689(199903)9:1<27::AID-STVR172>3.0.CO;2-B"},{"key":"e_1_2_1_73_1","volume-title":"FME '93: Industrial Strength Formal Methods, J. C. P. Woodcock and P. G. Larsen, Eds. Lecture Notes in Computer Science","volume":"670","author":"Dick J.","unstructured":"Dick , J. and Faivre , A . 1993. Automating the generation and sequencing of test cases from model based specifications . In FME '93: Industrial Strength Formal Methods, J. C. P. Woodcock and P. G. Larsen, Eds. Lecture Notes in Computer Science , vol. 670 . Springer-Verlag, Berlin, Germany, 268--284. Dick, J. and Faivre, A. 1993. Automating the generation and sequencing of test cases from model based specifications. In FME '93: Industrial Strength Formal Methods, J. C. P. Woodcock and P. G. Larsen, Eds. Lecture Notes in Computer Science, vol. 670. Springer-Verlag, Berlin, Germany, 268--284."},{"key":"e_1_2_1_74_1","volume-title":"Notes of structured programming","author":"Dijkstra E. W.","unstructured":"Dijkstra , E. W. 1972. Notes of structured programming . In Structured Programming, O. J. Dahl, E. W. Dijkstra, and C. A. R. Hoare, Eds. Academic Press , New York, NY . Dijkstra, E. W. 1972. Notes of structured programming. In Structured Programming, O. J. Dahl, E. W. Dijkstra, and C. A. R. Hoare, Eds. Academic Press, New York, NY."},{"key":"e_1_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1145\/120807.120822"},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1145\/192218.192221"},{"key":"e_1_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2004.1275300"},{"key":"e_1_2_1_78_1","unstructured":"Eilenberg S. 1974. Automata languages and machines. Vol. A. Academic Press New York NY.   Eilenberg S. 1974. Automata languages and machines. Vol. A. Academic Press New York NY."},{"key":"e_1_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-003-0042-x"},{"key":"e_1_2_1_80_1","volume-title":"Proceedings of the International Internet & Software Quality Week Europe Conference.","author":"El-Far I. K.","unstructured":"El-Far , I. K. , Thompson , H. H. , and Mottay , F. E . 2001. Experiences in testing pocket PS applications . In Proceedings of the International Internet & Software Quality Week Europe Conference. El-Far, I. K., Thompson, H. H., and Mottay, F. E. 2001. Experiences in testing pocket PS applications. In Proceedings of the International Internet & Software Quality Week Europe Conference."},{"key":"e_1_2_1_81_1","volume-title":"Handbook of Theoretical Computer Science.","author":"Emerson E. A.","unstructured":"Emerson , E. A. 1990. Temporal and modal logic . In Handbook of Theoretical Computer Science. Vol. B. North-Holland, Amsterdam, The Netherlands, 995-- 1072 . Emerson, E. A. 1990. Temporal and modal logic. In Handbook of Theoretical Computer Science. Vol. B. North-Holland, Amsterdam, The Netherlands, 995--1072."},{"key":"e_1_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2002.1049402"},{"key":"e_1_2_1_83_1","volume-title":"Proceedings of the IEEE Real-Time Systems Symposium. 220--229","author":"En-Nouaary A.","unstructured":"En-Nouaary , A. , Dssouli , R. , Khendek , F. , and Elqortobi , A . 1998. Timed test cases generation based on state characterization technique . In Proceedings of the IEEE Real-Time Systems Symposium. 220--229 . En-Nouaary, A., Dssouli, R., Khendek, F., and Elqortobi, A. 1998. Timed test cases generation based on state characterization technique. In Proceedings of the IEEE Real-Time Systems Symposium. 220--229."},{"key":"e_1_2_1_84_1","volume-title":"Third International Workshop, TACAS '97","volume":"1217","author":"Engels A.","unstructured":"Engels , A. , Feijs , L. M. G. , and Mauw , S . 1997. Test generation for intelligent networks using model checking. In Tools and Algorithms for Construction and Analysis of Systems , Third International Workshop, TACAS '97 . Lecture Notes in Computer Science , vol. 1217 . Springer-Verlag, Berlin, Germany, 384--398. Engels, A., Feijs, L. M. G., and Mauw, S. 1997. Test generation for intelligent networks using model checking. In Tools and Algorithms for Construction and Analysis of Systems, Third International Workshop, TACAS '97. Lecture Notes in Computer Science, vol. 1217. Springer-Verlag, Berlin, Germany, 384--398."},{"key":"e_1_2_1_85_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSM.2001.972767"},{"key":"e_1_2_1_86_1","doi-asserted-by":"publisher","DOI":"10.1147\/sj.411.0089"},{"key":"e_1_2_1_87_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2002.1020298"},{"key":"e_1_2_1_88_1","volume-title":"8th International Conference, CAV'96","author":"Fernandez J.-C.","year":"1996","unstructured":"Fernandez , J.-C. , Jard , C. , Jeron , T. , and Viho , G . 1996. Using on-the-fly verification techniques for the generation of test suites. In Computer Aided Verification , 8th International Conference, CAV'96 , New Brunswick, NJ, USA, July 31-- August 3, 1996 , Proceedings, R. Alur and T. A. Henzinger, Eds. Lecture Notes in Computer Science, vol. 1102. Springer, Berlin, Germany, 348--359. Fernandez, J.-C., Jard, C., Jeron, T., and Viho, G. 1996. Using on-the-fly verification techniques for the generation of test suites. In Computer Aided Verification, 8th International Conference, CAV'96, New Brunswick, NJ, USA, July 31-- August 3, 1996, Proceedings, R. Alur and T. A. Henzinger, Eds. Lecture Notes in Computer Science, vol. 1102. Springer, Berlin, Germany, 348--359."},{"key":"e_1_2_1_89_1","doi-asserted-by":"publisher","DOI":"10.1145\/48529.48530"},{"key":"e_1_2_1_90_1","volume-title":"Proceedings of the Ada-Europe'96","author":"Fletcher R.","unstructured":"Fletcher , R. and Sajeev , A. S. M. 1996. A framework for testing object-oriented software using formal specifications . In Proceedings of the Ada-Europe'96 , International Conference on Reliable Software Technologies (Montreux, Switzerland). 159--170. Fletcher, R. and Sajeev, A. S. M. 1996. A framework for testing object-oriented software using formal specifications. In Proceedings of the Ada-Europe'96, International Conference on Reliable Software Technologies (Montreux, Switzerland). 159--170."},{"key":"e_1_2_1_91_1","volume-title":"Failures-Divergence Refinement: FDR2 User Manual","author":"Formal Systems","unstructured":"Formal Systems (Europe) Ltd. 1997. Failures-Divergence Refinement: FDR2 User Manual . Formal Systems (Europe) Ltd . Oxford, U.K. Formal Systems (Europe) Ltd. 1997. Failures-Divergence Refinement: FDR2 User Manual. Formal Systems (Europe) Ltd. Oxford, U.K."},{"key":"e_1_2_1_92_1","volume-title":"Proceedings of the Formal Approaches to Software Testing, 4th International Workshop (FATES) Linz, Austria), 1--15","author":"Frantzen L.","unstructured":"Frantzen , L. , Tretmans , J. , and Willemse , T. A. C. 2004. Test generation based on symbolic specifications . In Proceedings of the Formal Approaches to Software Testing, 4th International Workshop (FATES) Linz, Austria), 1--15 . Frantzen, L., Tretmans, J., and Willemse, T. A. C. 2004. Test generation based on symbolic specifications. In Proceedings of the Formal Approaches to Software Testing, 4th International Workshop (FATES) Linz, Austria), 1--15."},{"key":"e_1_2_1_93_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.87284"},{"key":"e_1_2_1_94_1","doi-asserted-by":"publisher","DOI":"10.1145\/357139.357140"},{"key":"e_1_2_1_95_1","volume-title":"Proceedings of the International Symposium of Formal Methods Europe (FME). 410--429","author":"Garavel H.","unstructured":"Garavel , H. and Hermanns , H . 2002. On combining functional verification and performance evaluation using CADP . In Proceedings of the International Symposium of Formal Methods Europe (FME). 410--429 . Garavel, H. and Hermanns, H. 2002. On combining functional verification and performance evaluation using CADP. In Proceedings of the International Symposium of Formal Methods Europe (FME). 410--429."},{"key":"e_1_2_1_96_1","volume-title":"ESEC '99","volume":"1687","author":"Gargantini A.","unstructured":"Gargantini , A. and Heitmeyer , C . 1999. Using model checking to generate tests from requirements specifications . In ESEC '99 . Lecture Notes in Computer Science , vol. 1687 . Springer-Verlag, Berlin, Germany, 146--162. Gargantini, A. and Heitmeyer, C. 1999. Using model checking to generate tests from requirements specifications. In ESEC '99. Lecture Notes in Computer Science, vol. 1687. Springer-Verlag, Berlin, Germany, 146--162."},{"key":"e_1_2_1_97_1","volume-title":"TAPSOFT '95","author":"Gaudel M.-C.","unstructured":"Gaudel , M.-C. 1995. Testing can be formal too . In TAPSOFT '95 . Springer-Verlag , Berlin, Germany , 82--96. Gaudel, M.-C. 1995. Testing can be formal too. In TAPSOFT '95. Springer-Verlag, Berlin, Germany, 82--96."},{"key":"e_1_2_1_98_1","series-title":"Lecture Notes in Computer Science","volume-title":"Ada--Europe","author":"Gaudel M.-C.","unstructured":"Gaudel , M.-C. 2001. Testing from formal specifications, a generic approach . In Ada--Europe . Lecture Notes in Computer Science , vol. 2043 . Springer-Verlag , Berlin, Germany , 35--48. Gaudel, M.-C. 2001. Testing from formal specifications, a generic approach. In Ada--Europe. Lecture Notes in Computer Science, vol. 2043. Springer-Verlag, Berlin, Germany, 35--48."},{"key":"e_1_2_1_99_1","doi-asserted-by":"publisher","DOI":"10.1007\/s001650050026"},{"key":"e_1_2_1_100_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.44359"},{"key":"e_1_2_1_101_1","volume-title":"Introduction to the Theory of Finite-State Machines","author":"Gill A.","unstructured":"Gill , A. 1962. Introduction to the Theory of Finite-State Machines . McGraw-Hill , New York, NY . Gill, A. 1962. Introduction to the Theory of Finite-State Machines. McGraw-Hill, New York, NY."},{"key":"e_1_2_1_102_1","doi-asserted-by":"publisher","DOI":"10.1109\/MRA.2005.1411415"},{"key":"e_1_2_1_103_1","series-title":"Lecture Notes in Computer Science","volume-title":"Partial-Order Methods for the Verification of Concurrent Systems\u2014An Approach to the State-Explosion Problem","author":"Godefroid P.","unstructured":"Godefroid , P. 1996. Partial-Order Methods for the Verification of Concurrent Systems\u2014An Approach to the State-Explosion Problem . Lecture Notes in Computer Science , vol. 1032 . Springer-Verlag, New York , NY. Godefroid, P. 1996. Partial-Order Methods for the Verification of Concurrent Systems\u2014An Approach to the State-Explosion Problem. Lecture Notes in Computer Science, vol. 1032. Springer-Verlag, New York, NY."},{"key":"e_1_2_1_104_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263717"},{"key":"e_1_2_1_105_1","volume-title":"Hybrid Systems III. Lecture Notes in Computer Science","volume":"1066","author":"Godhavn J.-M.","unstructured":"Godhavn , J.-M. , Lauvdal , T. , and Egeland , O . 1996. Hybrid control in sea traffic management systems . In Hybrid Systems III. Lecture Notes in Computer Science , vol. 1066 , Springer, Berlin, Germany, 149--160. Godhavn, J.-M., Lauvdal, T., and Egeland, O. 1996. Hybrid control in sea traffic management systems. In Hybrid Systems III. Lecture Notes in Computer Science, vol. 1066, Springer, Berlin, Germany, 149--160."},{"key":"e_1_2_1_106_1","volume-title":"OBJ: Algebraic Specifications in Action","author":"Goguen J. A.","year":"2000","unstructured":"Goguen , J. A. and Malcolm , G . 2000 . Software Engineering with OBJ: Algebraic Specifications in Action . Kluwer Academic Publishers, Dordrecht, The Netherlands . Goguen, J. A. and Malcolm, G. 2000. Software Engineering with OBJ: Algebraic Specifications in Action. Kluwer Academic Publishers, Dordrecht, The Netherlands."},{"key":"e_1_2_1_107_1","volume-title":"Proceedings of the IEEE Conference on Specifications of Reliable Software. IEEE Computer Society Press","author":"Goguen J. A.","unstructured":"Goguen , J. A. and Tardo , J. J . 1979. An introduction to OBJ: A language for writing and testing formal algebraic specifications . In Proceedings of the IEEE Conference on Specifications of Reliable Software. IEEE Computer Society Press , Los Alamitos, CA, 170--189. Goguen, J. A. and Tardo, J. J. 1979. An introduction to OBJ: A language for writing and testing formal algebraic specifications. In Proceedings of the IEEE Conference on Specifications of Reliable Software. IEEE Computer Society Press, Los Alamitos, CA, 170--189."},{"key":"e_1_2_1_108_1","doi-asserted-by":"publisher","DOI":"10.1109\/T-C.1970.222975"},{"key":"e_1_2_1_109_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1975.6312836"},{"key":"e_1_2_1_110_1","doi-asserted-by":"publisher","DOI":"10.1145\/271771.271790"},{"key":"e_1_2_1_111_1","doi-asserted-by":"publisher","DOI":"10.1145\/566172.566190"},{"key":"e_1_2_1_112_1","volume-title":"TACAS","volume":"2280","author":"Groce A.","year":"2002","unstructured":"Groce , A. , Peled , D. , and Yannakakis , M . 2002. Adaptive model checking . In TACAS 2002 . Lecture Notes in Computer Science , vol. 2280 . Springer-Verlag, Berlin, Germany, 357--370. Groce, A., Peled, D., and Yannakakis, M. 2002. Adaptive model checking. In TACAS 2002. Lecture Notes in Computer Science, vol. 2280. Springer-Verlag, Berlin, Germany, 357--370."},{"key":"e_1_2_1_113_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-005-0059-8"},{"key":"e_1_2_1_114_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(97)00006-3"},{"key":"e_1_2_1_115_1","volume-title":"Proceedings of the 2nd IEE\/BCS Conference on Software Engineering. 159--163","author":"Hall P. A. V.","year":"1988","unstructured":"Hall , P. A. V. 1988 . Towards testing with respect to formal specification . In Proceedings of the 2nd IEE\/BCS Conference on Software Engineering. 159--163 . Hall, P. A. V. 1988. Towards testing with respect to formal specification. In Proceedings of the 2nd IEE\/BCS Conference on Software Engineering. 159--163."},{"key":"e_1_2_1_116_1","doi-asserted-by":"publisher","DOI":"10.1145\/75308.75313"},{"key":"e_1_2_1_117_1","volume-title":"Improving test suites via generated specifications. Tech. rep. 848","author":"Harder M.","unstructured":"Harder , M. 2002. Improving test suites via generated specifications. Tech. rep. 848 . Department of EECS. Cambridge , MA. Harder, M. 2002. Improving test suites via generated specifications. Tech. rep. 848. Department of EECS. Cambridge, MA."},{"key":"e_1_2_1_118_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.596624"},{"key":"e_1_2_1_119_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2004.1265732"},{"key":"e_1_2_1_120_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050043"},{"key":"e_1_2_1_121_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:FORM.0000017721.39909.4b"},{"key":"e_1_2_1_122_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1986.6312926"},{"key":"e_1_2_1_123_1","volume-title":"ZUM '97: The Z Formal Specification Notation, J. P. Bowen, M. G. Hinchey, and D. Till, Eds. Lecture Notes in Computer Science","volume":"1212","author":"Helke S.","unstructured":"Helke , S. , Neustupny , T. , and Santen , T . 1997. Automating test case generation from Z specifications with Isabelle . In ZUM '97: The Z Formal Specification Notation, J. P. Bowen, M. G. Hinchey, and D. Till, Eds. Lecture Notes in Computer Science , vol. 1212 . Springer-Verlag, Berlin, Germany, 52--71. Helke, S., Neustupny, T., and Santen, T. 1997. Automating test case generation from Z specifications with Isabelle. In ZUM '97: The Z Formal Specification Notation, J. P. Bowen, M. G. Hinchey, and D. Till, Eds. Lecture Notes in Computer Science, vol. 1212. Springer-Verlag, Berlin, Germany, 52--71."},{"key":"e_1_2_1_124_1","doi-asserted-by":"publisher","DOI":"10.1109\/SWCT.1964.8"},{"key":"e_1_2_1_125_1","volume-title":"SPIN","volume":"2648","author":"Henzinger T.","year":"2003","unstructured":"Henzinger , T. , Jhala , R. , Majumdar , R. , and Sutre , G . 2003. Software verification with Blast . In SPIN 2003 . Lecture Notes in Computer Science , vol. 2648 . Springer-Verlag, Berlin, Germany, 235--239. Henzinger, T., Jhala, R., Majumdar, R., and Sutre, G. 2003. Software verification with Blast. In SPIN 2003. Lecture Notes in Computer Science, vol. 2648. Springer-Verlag, Berlin, Germany, 235--239."},{"key":"e_1_2_1_126_1","volume-title":"CONCUR '96","volume":"1119","author":"Henzinger T. A.","unstructured":"Henzinger , T. A. , Kupferman , O. , and Vardi , M. Y . 1996. A space-efficient on-the-fly algorithm for real-time model checking . In CONCUR '96 . Lecture Notes in Computer Science , vol. 1119 . Springer-Verlag, Berlin, Germany, 514--529. Henzinger, T. A., Kupferman, O., and Vardi, M. Y. 1996. A space-efficient on-the-fly algorithm for real-time model checking. In CONCUR '96. Lecture Notes in Computer Science, vol. 1119. Springer-Verlag, Berlin, Germany, 514--529."},{"key":"e_1_2_1_127_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/40.4.220"},{"key":"e_1_2_1_128_1","doi-asserted-by":"publisher","DOI":"10.1002\/(SICI)1099-1689(199703)7:1<19::AID-STVR124>3.0.CO;2-N"},{"key":"e_1_2_1_129_1","first-page":"443","article-title":"Checking states and transitions of a set of communicating finite state machines","volume":"24","author":"Hierons R. M.","year":"2001","unstructured":"Hierons , R. M. 2001 . Checking states and transitions of a set of communicating finite state machines . Microproc. Microsyst. (Special Issue on Testing and Testing Techniques for Real-Time Embedded Software Systems) 24 , 9, 443 -- 452 . Hierons, R. M. 2001. Checking states and transitions of a set of communicating finite state machines. Microproc. Microsyst. (Special Issue on Testing and Testing Techniques for Real-Time Embedded Software Systems) 24, 9, 443--452.","journal-title":"Microproc. Microsyst. (Special Issue on Testing and Testing Techniques for Real-Time Embedded Software Systems)"},{"key":"e_1_2_1_130_1","doi-asserted-by":"publisher","DOI":"10.1145\/606612.606615"},{"key":"e_1_2_1_131_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2004.03.003"},{"key":"e_1_2_1_132_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2004.85"},{"key":"e_1_2_1_133_1","doi-asserted-by":"publisher","DOI":"10.1007\/s001650070003"},{"key":"e_1_2_1_134_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.04.002"},{"key":"e_1_2_1_135_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.comnet.2003.06.001"},{"key":"e_1_2_1_136_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0950-5849(00)00145-2"},{"key":"e_1_2_1_137_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2006.80"},{"key":"e_1_2_1_138_1","volume-title":"Communicating Sequential Processes","author":"Hoare C. A. R.","unstructured":"Hoare , C. A. R. 1985. Communicating Sequential Processes . Prentice Hall International Series in Computer Science. Prentice Hall , Englewood Cliffs, NJ. Hoare, C. A. R. 1985. Communicating Sequential Processes. Prentice Hall International Series in Computer Science. Prentice Hall, Englewood Cliffs, NJ."},{"key":"e_1_2_1_139_1","volume-title":"Eds. Lecture Notes in Computer Science","volume":"1052","author":"Hoare C. A. R.","year":"1996","unstructured":"Hoare , C. A. R. 1996 . How did software get so reliable without proof&quest; In Cost 237 Workshop, D. Hutchison, H. Christiansen, G. Coulson, and A. S. Danthine , Eds. Lecture Notes in Computer Science , vol. 1052 . Springer, Berlin, Germany, 1--17. Hoare, C. A. R. 1996. How did software get so reliable without proof&quest; In Cost 237 Workshop, D. Hutchison, H. Christiansen, G. Coulson, and A. S. Danthine, Eds. Lecture Notes in Computer Science, vol. 1052. Springer, Berlin, Germany, 1--17."},{"key":"e_1_2_1_140_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-3435-0"},{"key":"e_1_2_1_141_1","volume-title":"The Spin Model Checker: Primer and Reference Manual","author":"Holzmann G.","unstructured":"Holzmann , G. 2003. The Spin Model Checker: Primer and Reference Manual . Addison-Wesley , Reading, MA . Holzmann, G. 2003. The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, Reading, MA."},{"key":"e_1_2_1_142_1","doi-asserted-by":"publisher","DOI":"10.1145\/242224.242379"},{"key":"e_1_2_1_143_1","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.228"},{"key":"e_1_2_1_144_1","volume-title":"Proceedings of ICSE","author":"Hong H.","year":"2003","unstructured":"Hong , H. , Cha , S. , Lee , I. , Sokolsky , O. , and Ural , H . 2003. Data flow testing as model checking . In Proceedings of ICSE 2003 . IEEE Computer Society Press, Los Alamitos, CA, 232--243. Hong, H., Cha, S., Lee, I., Sokolsky, O., and Ural, H. 2003. Data flow testing as model checking. In Proceedings of ICSE 2003. IEEE Computer Society Press, Los Alamitos, CA, 232--243."},{"key":"e_1_2_1_145_1","volume-title":"TACAS","volume":"2280","author":"Hong H.","year":"2002","unstructured":"Hong , H. , Lee , I. , Sokolsky , O. , and Ural , H . 2002. A temporal logic based theory of test coverage and generation . In TACAS 2002 . Lecture Notes in Computer Science , vol. 2280 . Springer-Verlag, Berlin, Germany, 327--341. Hong, H., Lee, I., Sokolsky, O., and Ural, H. 2002. A temporal logic based theory of test coverage and generation. In TACAS 2002. Lecture Notes in Computer Science, vol. 2280. Springer-Verlag, Berlin, Germany, 327--341."},{"key":"e_1_2_1_146_1","volume-title":"FATES '01","volume":"4","author":"Hong H. S.","unstructured":"Hong , H. S. , Lee , I. , Sokolsky , O. , and Cha , S. D . 2001. Automatic test generation from Statecharts using model checking . In FATES '01 . BRICS Notes Series , vol. NS-01- 4 . BRICS, Aarhus, Denmark, 15--30. Hong, H. S., Lee, I., Sokolsky, O., and Cha, S. D. 2001. Automatic test generation from Statecharts using model checking. In FATES '01. BRICS Notes Series, vol. NS-01-4. BRICS, Aarhus, Denmark, 15--30."},{"key":"e_1_2_1_147_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00402650"},{"key":"e_1_2_1_148_1","doi-asserted-by":"publisher","DOI":"10.1109\/52.896246"},{"key":"e_1_2_1_149_1","doi-asserted-by":"publisher","DOI":"10.1109\/T-C.1971.223100"},{"key":"e_1_2_1_150_1","volume-title":"Proceedings of the 4th International Symposium of Formal Methods Europe (FME). 122--141","author":"Huber F.","unstructured":"Huber , F. , Sch\u00e4tz , B. , and Einert , G . 1997. Consistent graphical specification of distributed systems . In Proceedings of the 4th International Symposium of Formal Methods Europe (FME). 122--141 . Huber, F., Sch\u00e4tz, B., and Einert, G. 1997. Consistent graphical specification of distributed systems. In Proceedings of the 4th International Symposium of Formal Methods Europe (FME). 122--141."},{"key":"e_1_2_1_151_1","doi-asserted-by":"publisher","DOI":"10.1145\/229000.226301"},{"key":"e_1_2_1_152_1","volume-title":"Proceedings of the 6th IEEE International Symposium on Object-Oriented Real-Time Distributed Computing (ISORC). 93--98","author":"Hur Y.","unstructured":"Hur , Y. , Fierro , R. B. , and Lee , I . 2003. Modeling distributed autonomous robots using CHARON: Formation control case study . In Proceedings of the 6th IEEE International Symposium on Object-Oriented Real-Time Distributed Computing (ISORC). 93--98 . Hur, Y., Fierro, R. B., and Lee, I. 2003. Modeling distributed autonomous robots using CHARON: Formation control case study. In Proceedings of the 6th IEEE International Symposium on Object-Oriented Real-Time Distributed Computing (ISORC). 93--98."},{"key":"e_1_2_1_153_1","doi-asserted-by":"publisher","DOI":"10.1080\/00207169708804559"},{"key":"e_1_2_1_154_1","doi-asserted-by":"publisher","DOI":"10.1007\/s001650070004"},{"key":"e_1_2_1_155_1","volume-title":"Open Systems Interconnection\u2014LOTOS\u2014A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour","author":"Information Processing Systems","unstructured":"ISO. 1989a. ISO 8807:1989 Information Processing Systems , Open Systems Interconnection\u2014LOTOS\u2014A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour . ISO , Geneva, Switzerland . ISO. 1989a. ISO 8807:1989 Information Processing Systems, Open Systems Interconnection\u2014LOTOS\u2014A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour. ISO, Geneva, Switzerland."},{"key":"e_1_2_1_156_1","unstructured":"ISO. 1989b. ISO 9074; Estelle\u2014A Formal Description Technique Based on an Extended State Transition Model. ISO Geneva Switzerland.  ISO. 1989b. ISO 9074; Estelle\u2014A Formal Description Technique Based on an Extended State Transition Model. ISO Geneva Switzerland."},{"key":"e_1_2_1_157_1","volume-title":"International Telecommunications Union","author":"Recommendation Z.","unstructured":"ITU-T. 1997. Recommendation Z. 500 Framework on Formal Methods in Conformance Testing. International Telecommunications Union , Geneva, Switzerland . ITU-T. 1997. Recommendation Z.500 Framework on Formal Methods in Conformance Testing. International Telecommunications Union, Geneva, Switzerland."},{"key":"e_1_2_1_158_1","volume-title":"International Telecommunications Union","author":"Recommendation Z.","unstructured":"ITU-T. 1999. Recommendation Z. 100 Specification and Description Language (SDL). International Telecommunications Union , Geneva, Switzerland . ITU-T. 1999. Recommendation Z.100 Specification and Description Language (SDL). International Telecommunications Union, Geneva, Switzerland."},{"key":"e_1_2_1_159_1","doi-asserted-by":"publisher","DOI":"10.1145\/347324.383378"},{"key":"e_1_2_1_160_1","volume-title":"Proceedings of the 7th International Computer Software and Applications Conference (COMPSAC). IEEE Computer Society Press","author":"Jalote P.","year":"1983","unstructured":"Jalote , P. 1983 . Specification and testing of abstract data types . In Proceedings of the 7th International Computer Software and Applications Conference (COMPSAC). IEEE Computer Society Press , Los Alamitos, CA, 508--511. Jalote, P. 1983. Specification and testing of abstract data types. In Proceedings of the 7th International Computer Software and Applications Conference (COMPSAC). IEEE Computer Society Press, Los Alamitos, CA, 508--511."},{"key":"e_1_2_1_161_1","volume-title":"Proceedings of the 12th International Computer Software and Applications Conference (COMPSAC). IEEE Computer Society Press","author":"Jalote P.","unstructured":"Jalote , P. and Caballero , M. G . 1988. Automated testcase generation for data abstraction . In Proceedings of the 12th International Computer Software and Applications Conference (COMPSAC). IEEE Computer Society Press , Los Alamitos, CA, 205--210. Jalote, P. and Caballero, M. G. 1988. Automated testcase generation for data abstraction. In Proceedings of the 12th International Computer Software and Applications Conference (COMPSAC). IEEE Computer Society Press, Los Alamitos, CA, 205--210."},{"key":"e_1_2_1_162_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-004-0153-x"},{"key":"e_1_2_1_163_1","volume-title":"Systematic Software Development using VDM","author":"Jones C. B.","unstructured":"Jones , C. B. 1991. Systematic Software Development using VDM , 2 nd ed. Prentice Hall International Series in Computer Science. Prentice Hall , Englewood Cliffs, NJ. Jones, C. B. 1991. Systematic Software Development using VDM, 2nd ed. Prentice Hall International Series in Computer Science. Prentice Hall, Englewood Cliffs, NJ.","edition":"2"},{"key":"e_1_2_1_164_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1985.231535"},{"key":"e_1_2_1_165_1","doi-asserted-by":"crossref","unstructured":"Kerbrat A. J\u00e9ron T. and Groz R. 1999. Automated test generation from SDL specifications. In SDL For. 135--152.  Kerbrat A. J\u00e9ron T. and Groz R. 1999. Automated test generation from SDL specifications. In SDL For. 135--152.","DOI":"10.1016\/B978-044450228-5\/50011-4"},{"key":"e_1_2_1_166_1","unstructured":"Kernighan B. W. and Plauger P. J. 1981. Software Tools in Pascal. Addison-Wesley Reading MA.   Kernighan B. W. and Plauger P. J. 1981. Software Tools in Pascal. Addison-Wesley Reading MA."},{"key":"e_1_2_1_167_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.879807"},{"key":"e_1_2_1_168_1","volume-title":"Switching and Finite State Automata Theory","author":"Kohavi Z.","unstructured":"Kohavi , Z. 1978. Switching and Finite State Automata Theory . McGraw-Hill, New York , NY. Kohavi, Z. 1978. Switching and Finite State Automata Theory. McGraw-Hill, New York, NY."},{"key":"e_1_2_1_169_1","doi-asserted-by":"publisher","DOI":"10.1109\/TMECH.2005.848289"},{"key":"e_1_2_1_170_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/44.5.435"},{"key":"e_1_2_1_171_1","volume-title":"Proceedings of the 11th International SPIN Workshop. 109--126","author":"Krichen M.","unstructured":"Krichen , M. and Tripakis , S . 2004. Black-box conformance testing for real-time systems . In Proceedings of the 11th International SPIN Workshop. 109--126 . Krichen, M. and Tripakis, S. 2004. Black-box conformance testing for real-time systems. In Proceedings of the 11th International SPIN Workshop. 109--126."},{"key":"e_1_2_1_172_1","volume-title":"Proceedings of the 17th IFIP TC6\/WG 6.1 International Conference on Testing of Communicating Systems (TestCom). 209--225","author":"Krichen M.","unstructured":"Krichen , M. and Tripakis , S . 2005. An expressive and implementable formal framework for testing real-time systems . In Proceedings of the 17th IFIP TC6\/WG 6.1 International Conference on Testing of Communicating Systems (TestCom). 209--225 . Krichen, M. and Tripakis, S. 2005. An expressive and implementable formal framework for testing real-time systems. In Proceedings of the 17th IFIP TC6\/WG 6.1 International Conference on Testing of Communicating Systems (TestCom). 209--225."},{"key":"e_1_2_1_173_1","doi-asserted-by":"publisher","DOI":"10.1145\/322993.322996"},{"key":"e_1_2_1_174_1","doi-asserted-by":"publisher","DOI":"10.1145\/1072997.1072998"},{"key":"e_1_2_1_175_1","volume-title":"Protocol Specification, Testing, and Verification XI","author":"Leduc G.","unstructured":"Leduc , G. 1991. Conformance relation, associated equivalence, and a new canonical tester in LOTOS . In Protocol Specification, Testing, and Verification XI . Elsevier (North-Holland) , Amsterdam, The Netherlands, 249--264. Leduc, G. 1991. Conformance relation, associated equivalence, and a new canonical tester in LOTOS. In Protocol Specification, Testing, and Verification XI. Elsevier (North-Holland), Amsterdam, The Netherlands, 249--264."},{"key":"e_1_2_1_176_1","doi-asserted-by":"publisher","DOI":"10.1109\/12.272431"},{"key":"e_1_2_1_177_1","doi-asserted-by":"publisher","DOI":"10.1109\/5.533956"},{"key":"e_1_2_1_178_1","volume-title":"Lecture Notes in Computer Science","volume":"2391","author":"Legeard B.","unstructured":"Legeard , B. , Peureux , F. , and Utting , M . 2002a. Automated boundary testing from Z and B. In Formal Methods Europe (FME 02) . Lecture Notes in Computer Science , vol. 2391 . Springer, Berlin, Germany, 21--40. Legeard, B., Peureux, F., and Utting, M. 2002a. Automated boundary testing from Z and B. In Formal Methods Europe (FME 02). Lecture Notes in Computer Science, vol. 2391. Springer, Berlin, Germany, 21--40."},{"key":"e_1_2_1_179_1","volume-title":"Proceedings of the Conference on Formal Specification and Development in Z and B (ZB). 309--329","author":"Legeard B.","unstructured":"Legeard , B. , Peureux , F. , and Utting , M . 2002b. A comparison of the BTT and TTF test-generation methods . In Proceedings of the Conference on Formal Specification and Development in Z and B (ZB). 309--329 . Legeard, B., Peureux, F., and Utting, M. 2002b. A comparison of the BTT and TTF test-generation methods. In Proceedings of the Conference on Formal Specification and Development in Z and B (ZB). 309--329."},{"key":"e_1_2_1_180_1","volume-title":"Proceedings of the 13th International Symposium on Software Reliability Engineering (ISSRE). 3--14","author":"Lestiennes G.","unstructured":"Lestiennes , G. and Gaudel , M . -C. 2002. Testing processes from formal specifications with inputs, outputs and data types . In Proceedings of the 13th International Symposium on Software Reliability Engineering (ISSRE). 3--14 . Lestiennes, G. and Gaudel, M.-C. 2002. Testing processes from formal specifications with inputs, outputs and data types. In Proceedings of the 13th International Symposium on Software Reliability Engineering (ISSRE). 3--14."},{"key":"e_1_2_1_181_1","doi-asserted-by":"publisher","DOI":"10.1145\/318593.318622"},{"key":"e_1_2_1_182_1","doi-asserted-by":"publisher","DOI":"10.1145\/1062455.1062461"},{"key":"e_1_2_1_183_1","doi-asserted-by":"publisher","DOI":"10.5555\/647544.730475"},{"key":"e_1_2_1_184_1","volume-title":"APSEC 2000: Proceedings of the 7th Asia-Pacific Software Engineering Conference. IEEE Computer Society Press","author":"Liu S.","unstructured":"Liu , S. , Fukuzaki , T. , and Miyamoto , K . 2000. A GUI and testing tool for SOFL . In APSEC 2000: Proceedings of the 7th Asia-Pacific Software Engineering Conference. IEEE Computer Society Press , Los Alamitos, CA, 421--425. Liu, S., Fukuzaki, T., and Miyamoto, K. 2000. A GUI and testing tool for SOFL. In APSEC 2000: Proceedings of the 7th Asia-Pacific Software Engineering Conference. IEEE Computer Society Press, Los Alamitos, CA, 421--425."},{"key":"e_1_2_1_185_1","volume-title":"Validation of Stochastic Systems. Lecture Notes in Computer Science","volume":"2925","author":"L\u00f3pez N.","unstructured":"L\u00f3pez , N. and N\u00fa\u00f1ez , M . 2004. An overview of probabilistic process algebras and their equivalences . In Validation of Stochastic Systems. Lecture Notes in Computer Science , vol. 2925 . Springer, Berlin, Germany, 89--123. L\u00f3pez, N. and N\u00fa\u00f1ez, M. 2004. An overview of probabilistic process algebras and their equivalences. In Validation of Stochastic Systems. Lecture Notes in Computer Science, vol. 2925. Springer, Berlin, Germany, 89--123."},{"key":"e_1_2_1_186_1","volume-title":"Proceedings of the 7th IFIP Workshop on Protocol Test Systems. Chapman and Hall","author":"Luo G. L.","year":"1994","unstructured":"Luo , G. L. , Petrenko , A. , and von Bochmann , G. 1994 a. Selecting test sequences for partially-specified nondeterministic finite state machines . In Proceedings of the 7th IFIP Workshop on Protocol Test Systems. Chapman and Hall , London, U.K., 95--110. Luo, G. L., Petrenko, A., and von Bochmann, G. 1994a. Selecting test sequences for partially-specified nondeterministic finite state machines. In Proceedings of the 7th IFIP Workshop on Protocol Test Systems. Chapman and Hall, London, U.K., 95--110."},{"key":"e_1_2_1_187_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.265636"},{"key":"e_1_2_1_188_1","volume-title":"Proceedings of the 15th European Conference on Artificial Intelligence (ECAI). 166--170","author":"Lynce I.","unstructured":"Lynce , I. and Marques-Silva , J . 2002. Building state-of-the-art sat solvers . In Proceedings of the 15th European Conference on Artificial Intelligence (ECAI). 166--170 . Lynce, I. and Marques-Silva, J. 2002. Building state-of-the-art sat solvers. In Proceedings of the 15th European Conference on Artificial Intelligence (ECAI). 166--170."},{"key":"e_1_2_1_189_1","volume-title":"FAHCI98: Proceedings of the Formal Aspects of Human Computer Interaction Workshop. British Computer Society","author":"MacColl I.","unstructured":"MacColl , I. and Carrington , D . 1998. Testing MATIS: A case study on specification-based testing of interactive systems . In FAHCI98: Proceedings of the Formal Aspects of Human Computer Interaction Workshop. British Computer Society , Swindon, U.K., 57--69. MacColl, I. and Carrington, D. 1998. Testing MATIS: A case study on specification-based testing of interactive systems. In FAHCI98: Proceedings of the Formal Aspects of Human Computer Interaction Workshop. British Computer Society, Swindon, U.K., 57--69."},{"key":"e_1_2_1_190_1","doi-asserted-by":"publisher","DOI":"10.5555\/646060.678683"},{"key":"e_1_2_1_191_1","volume-title":"Hybrid Systems. Lecture Notes in Computer Science","volume":"736","author":"Manna Z.","unstructured":"Manna , Z. and Pnueli , A . 1992. Verifying hybrid systems . In Hybrid Systems. Lecture Notes in Computer Science , vol. 736 . Springer-Verlag, Berlin, Germany, 4--35. Manna, Z. and Pnueli, A. 1992. Verifying hybrid systems. In Hybrid Systems. Lecture Notes in Computer Science, vol. 736. Springer-Verlag, Berlin, Germany, 4--35."},{"key":"e_1_2_1_192_1","doi-asserted-by":"crossref","unstructured":"Manna Z. and Pnueli A. 1995. Temporal Verification of Reactive Systems. Springer-Verlag Berlin Germany.   Manna Z. and Pnueli A. 1995. Temporal Verification of Reactive Systems. Springer-Verlag Berlin Germany.","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"e_1_2_1_193_1","volume-title":"Proceedings of the 16th IEEE Conference on Automated Software Engineering (ASE).","author":"Marinov D.","unstructured":"Marinov , D. and Khurshid , S . 2001. TestEra: A novel framework for automated testing of Java programs . In Proceedings of the 16th IEEE Conference on Automated Software Engineering (ASE). Marinov, D. and Khurshid, S. 2001. TestEra: A novel framework for automated testing of Java programs. In Proceedings of the 16th IEEE Conference on Automated Software Engineering (ASE)."},{"key":"e_1_2_1_194_1","doi-asserted-by":"publisher","DOI":"10.5555\/646619.697561"},{"key":"e_1_2_1_195_1","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/5625.003.0004"},{"key":"e_1_2_1_196_1","volume-title":"Symbolic Model Checking","author":"McMillan K. L.","unstructured":"McMillan , K. L. 1993. Symbolic Model Checking . Kluwer Academic Publishers, Dordrecht , The Netherlands . McMillan, K. L. 1993. Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht, The Netherlands."},{"key":"e_1_2_1_197_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1983.236869"},{"key":"e_1_2_1_199_1","volume-title":"Proceedings of the Test Symposium. (ATS) . 289--294","author":"Miao H.","unstructured":"Miao , H. , Gao , X. , and Liu , L . 1999. An approach to testing the nonexistence of initial state in Z specifications . In Proceedings of the Test Symposium. (ATS) . 289--294 . Miao, H., Gao, X., and Liu, L. 1999. An approach to testing the nonexistence of initial state in Z specifications. In Proceedings of the Test Symposium. (ATS) . 289--294."},{"key":"e_1_2_1_200_1","doi-asserted-by":"publisher","DOI":"10.5555\/647281.722760"},{"key":"e_1_2_1_201_1","volume-title":"Military Standard-Interoperability Standard for Digital Message Device Subsystems. Department of Defense","unstructured":"MIL-STD 188-220B. 1998. Military Standard-Interoperability Standard for Digital Message Device Subsystems. Department of Defense , Washington, DC . MIL-STD 188-220B. 1998. Military Standard-Interoperability Standard for Digital Message Device Subsystems. Department of Defense, Washington, DC."},{"key":"e_1_2_1_202_1","doi-asserted-by":"publisher","DOI":"10.1109\/90.222912"},{"key":"e_1_2_1_203_1","volume-title":"Communication and Concurrency","author":"Milner R.","unstructured":"Milner , R. 1989. Communication and Concurrency . Prentice Hall International Series in Computer Science. Prentice Hall , Englewood Cliffs, NJ. Milner, R. 1989. Communication and Concurrency. Prentice Hall International Series in Computer Science. Prentice Hall, Englewood Cliffs, NJ."},{"key":"e_1_2_1_204_1","volume-title":"Princeton","author":"Moore E. P.","unstructured":"Moore , E. P. 1956. Gedanken-experiments . In Automata Studies, C. Shannon and J. McCarthy, Eds. Princeton University Press, Princeton , NJ. Moore, E. P. 1956. Gedanken-experiments. In Automata Studies, C. Shannon and J. McCarthy, Eds. Princeton University Press, Princeton, NJ."},{"key":"e_1_2_1_205_1","series-title":"Lecture Notes in Computer Science","volume-title":"CASL Reference Manual: The Complete Documentation of the Common Algebraic Specification Language","author":"Mosses P. D.","unstructured":"Mosses , P. D. 2004. CASL Reference Manual: The Complete Documentation of the Common Algebraic Specification Language . Lecture Notes in Computer Science , vol. 2960 . Springer-Verlag, Berlin , Germany . Mosses, P. D. 2004. CASL Reference Manual: The Complete Documentation of the Common Algebraic Specification Language. Lecture Notes in Computer Science, vol. 2960. Springer-Verlag, Berlin, Germany."},{"key":"e_1_2_1_206_1","volume-title":"MOST media oriented system transport\u2014multimedia and control networking technology. MOST Cooperation","author":"Cooperation","unstructured":"MOST Cooperation . 2002. MOST media oriented system transport\u2014multimedia and control networking technology. MOST Cooperation . Karlsruhe, Germany . MOST Cooperation. 2002. MOST media oriented system transport\u2014multimedia and control networking technology. MOST Cooperation. Karlsruhe, Germany."},{"key":"e_1_2_1_207_1","volume-title":"11th International Conference of Z Users. Lecture Notes in Computer Science","volume":"1493","author":"Murray L.","unstructured":"Murray , L. , Carrington , D. , MacColl , I. , McDonald , J. , and Strooper , P . 1998. Formal derivation of finite state machines for class testing . In 11th International Conference of Z Users. Lecture Notes in Computer Science , vol. 1493 . Springer, Berlin, Germany, 42--59. Murray, L., Carrington, D., MacColl, I., McDonald, J., and Strooper, P. 1998. Formal derivation of finite state machines for class testing. In 11th International Conference of Z Users. Lecture Notes in Computer Science, vol. 1493. Springer, Berlin, Germany, 42--59."},{"key":"e_1_2_1_208_1","volume-title":"Proceedings of the IEEE Fault Tolerant Computing Conference. 238--243","author":"Naito S.","unstructured":"Naito , S. and Tsunoyama , M . 1981. Fault detection for sequential machines . In Proceedings of the IEEE Fault Tolerant Computing Conference. 238--243 . Naito, S. and Tsunoyama, M. 1981. Fault detection for sequential machines. In Proceedings of the IEEE Fault Tolerant Computing Conference. 238--243."},{"key":"e_1_2_1_209_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-002-0094-1"},{"key":"e_1_2_1_210_1","volume-title":"Lecture Notes in Computer Science","volume":"2767","author":"N\u00fa\u00f1ez M.","unstructured":"N\u00fa\u00f1ez , M. and Rodr\u00edguez , I . 2003. Towards testing stochastic timed systems. In Formal Techniques for Networked and Distributed Systems (FORTE 2003) . Lecture Notes in Computer Science , vol. 2767 . Springer, Berlin, Germany, 335--350. N\u00fa\u00f1ez, M. and Rodr\u00edguez, I. 2003. Towards testing stochastic timed systems. In Formal Techniques for Networked and Distributed Systems (FORTE 2003). Lecture Notes in Computer Science, vol. 2767. Springer, Berlin, Germany, 335--350."},{"key":"e_1_2_1_211_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0164-1212(99)00066-7"},{"key":"e_1_2_1_212_1","doi-asserted-by":"publisher","DOI":"10.1145\/62959.62964"},{"key":"e_1_2_1_213_1","volume-title":"Proceedings of the International Workshop on Automated Program Analysis, Testing and Verification","author":"Park D.","unstructured":"Park , D. , Stern , U. , Skakkebaek , J. U. , and Dill , D. L . 2000. Java model checking . In Proceedings of the International Workshop on Automated Program Analysis, Testing and Verification ( Limerick, Ireland). 74--82. Park, D., Stern, U., Skakkebaek, J. U., and Dill, D. L. 2000. Java model checking. In Proceedings of the International Workshop on Automated Program Analysis, Testing and Verification (Limerick, Ireland). 74--82."},{"key":"e_1_2_1_214_1","volume-title":"10th International Conference (CAV '98)","volume":"1427","author":"Peled D.","year":"1998","unstructured":"Peled , D. 1998 . Ten years of partial order reduction. In Computer Aided Verification , 10th International Conference (CAV '98) . Lecture Notes in Computer Science , vol. 1427 . Springer-Verlag, Berlin, Germany, 17--28. Peled, D. 1998. Ten years of partial order reduction. In Computer Aided Verification, 10th International Conference (CAV '98). Lecture Notes in Computer Science, vol. 1427. Springer-Verlag, Berlin, Germany, 17--28."},{"key":"e_1_2_1_215_1","volume-title":"Automata, Languages and Programming, 30th International Colloquium (ICALP","author":"Peled D.","year":"2003","unstructured":"Peled , D. 2003. Model checking and testing combined . In Automata, Languages and Programming, 30th International Colloquium (ICALP 2003 ). Lecture Notes in Computer Science, vol. 2719 . Springer-Verlag , Berlin, Germany, 47--63. Peled, D. 2003. Model checking and testing combined. In Automata, Languages and Programming, 30th International Colloquium (ICALP 2003). Lecture Notes in Computer Science, vol. 2719. Springer-Verlag, Berlin, Germany, 47--63."},{"key":"e_1_2_1_216_1","first-page":"225","article-title":"Black box checking","volume":"7","author":"Peled D.","year":"2002","unstructured":"Peled , D. , Vardi , M. , and Yannakakis , M. 2002 . Black box checking . J. Automat. Lang. Combin. 7 , 2, 225 -- 246 . Peled, D., Vardi, M., and Yannakakis, M. 2002. Black box checking. J. Automat. Lang. Combin. 7, 2, 225--246.","journal-title":"J. Automat. Lang. Combin."},{"key":"e_1_2_1_217_1","volume-title":"Protocol Test Systems. IFIP Transactions. North-Holland","author":"Petrenko A.","unstructured":"Petrenko , A. 1991. Checking experiments with protocol machines . In Protocol Test Systems. IFIP Transactions. North-Holland , Amsterdam, The Netherlands , 83--94. Petrenko, A. 1991. Checking experiments with protocol machines. In Protocol Test Systems. IFIP Transactions. North-Holland, Amsterdam, The Netherlands, 83--94."},{"key":"e_1_2_1_218_1","series-title":"Lecture Notes in Computer Science","volume-title":"Fault model-driven test derivation from finite state models: Annotated bibliography","author":"Petrenko A.","unstructured":"Petrenko , A. 2001. Fault model-driven test derivation from finite state models: Annotated bibliography . Lecture Notes in Computer Science , vol. 2067 . Springer , Berlin, Germany , 196--205. Petrenko, A. 2001. Fault model-driven test derivation from finite state models: Annotated bibliography. Lecture Notes in Computer Science, vol. 2067. Springer, Berlin, Germany, 196--205."},{"key":"e_1_2_1_219_1","unstructured":"Petrenko A. Boroday S. and Groz R. 1999. Configurations in EFSM. In Proceedings of the IFIP Joint International Conference on Formal Description Techniques for Distributed Systems (FORTE XII) and Communication Protocols and Protocol Specification Testing and Verification (PSTV XIX China). 5--24.   Petrenko A. Boroday S. and Groz R. 1999. Configurations in EFSM. In Proceedings of the IFIP Joint International Conference on Formal Description Techniques for Distributed Systems (FORTE XII) and Communication Protocols and Protocol Specification Testing and Verification (PSTV XIX China). 5--24."},{"key":"e_1_2_1_220_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2004.1265734"},{"key":"e_1_2_1_221_1","unstructured":"Petrenko A. Yevtushenko N. Lebedev A. and Das A. 1994. Nondeterministic state machines in protocol conformance testing. In Protocol Test Systems VI (C-19). Elsevier Science (North-Holland) Amsterdam The Netherlands 363--378.   Petrenko A. Yevtushenko N. Lebedev A. and Das A. 1994. Nondeterministic state machines in protocol conformance testing. In Protocol Test Systems VI (C-19). Elsevier Science (North-Holland) Amsterdam The Netherlands 363--378."},{"key":"e_1_2_1_222_1","doi-asserted-by":"publisher","DOI":"10.5555\/267295.267317"},{"key":"e_1_2_1_223_1","volume-title":"Protocol Test Systems VI. North-Holland","author":"Phalippou M.","unstructured":"Phalippou , M. 1994. Executable testers . In Protocol Test Systems VI. North-Holland , Amsterdam, The Netherlands , 35--50. Phalippou, M. 1994. Executable testers. In Protocol Test Systems VI. North-Holland, Amsterdam, The Netherlands, 35--50."},{"key":"e_1_2_1_224_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_1_225_1","doi-asserted-by":"publisher","DOI":"10.1145\/1062455.1062529"},{"key":"e_1_2_1_226_1","volume-title":"International Symposium on Programming. Lecture Notes in Computer Science","volume":"137","author":"Queille J. P.","unstructured":"Queille , J. P. and Sifakis , J . 1982. Specification and verification of concurrent systems in CESAR . In International Symposium on Programming. Lecture Notes in Computer Science , vol. 137 . Springer-Verlag, Berlin, Germany, 337--351. Queille, J. P. and Sifakis, J. 1982. Specification and verification of concurrent systems in CESAR. In International Symposium on Programming. Lecture Notes in Computer Science, vol. 137. Springer-Verlag, Berlin, Germany, 337--351."},{"key":"e_1_2_1_227_1","volume-title":"Hybrid Systems II. Lecture Notes in Computer Science","volume":"999","author":"Ravn A. P.","unstructured":"Ravn , A. P. , Rischel , H. , Conrad , F. , and Andersen , T. O . 1995. Hybrid control of a robot\u2014a case study . In Hybrid Systems II. Lecture Notes in Computer Science , vol. 999 , Springer, Berlin, Germany, 391--404. Ravn, A. P., Rischel, H., Conrad, F., and Andersen, T. O. 1995. Hybrid control of a robot\u2014a case study. In Hybrid Systems II. Lecture Notes in Computer Science, vol. 999, Springer, Berlin, Germany, 391--404."},{"key":"e_1_2_1_228_1","doi-asserted-by":"publisher","DOI":"10.1145\/288408.288439"},{"key":"e_1_2_1_229_1","doi-asserted-by":"publisher","DOI":"10.1145\/143062.143100"},{"key":"e_1_2_1_230_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1985.231892"},{"key":"e_1_2_1_231_1","unstructured":"Robinson A. and Voronkov A. 2001. Handbook of Automated Reasoning. MIT Press Cambridge MA.   Robinson A. and Voronkov A. 2001. Handbook of Automated Reasoning. MIT Press Cambridge MA."},{"key":"e_1_2_1_232_1","doi-asserted-by":"publisher","DOI":"10.1016\/0169-7552(88)90064-5"},{"key":"e_1_2_1_233_1","volume-title":"Proceedings of the 2nd International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE).","author":"Sato F.","unstructured":"Sato , F. , Munemori , J. , Ideguchi , T. , and Mizuno , T . 1989. Sequence generation tool for communication system . In Proceedings of the 2nd International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE). Sato, F., Munemori, J., Ideguchi, T., and Mizuno, T. 1989. Sequence generation tool for communication system. In Proceedings of the 2nd International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE)."},{"key":"e_1_2_1_234_1","doi-asserted-by":"crossref","unstructured":"Schmitt M. Ek A. Grabowski J. Hogrefe D. and Koch B. 1998. Autolink\u2014putting SDL-based test generation into practice. In Testing of Communicating Systems IFIP TC6 11th International Workshop on Testing Communicating Systems (IWTCS). Kluwer Academic Publishers Amsterdam The Netherlands 227--244.   Schmitt M. Ek A. Grabowski J. Hogrefe D. and Koch B. 1998. Autolink\u2014putting SDL-based test generation into practice. In Testing of Communicating Systems IFIP TC6 11th International Workshop on Testing Communicating Systems (IWTCS). Kluwer Academic Publishers Amsterdam The Netherlands 227--244.","DOI":"10.1007\/978-0-387-35381-4_14"},{"key":"e_1_2_1_235_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.16602"},{"key":"e_1_2_1_236_1","volume-title":"The Process Algebra Compiler User's Manual. Reactive Systems","author":"Sims S.","unstructured":"Sims , S. 1999. The Process Algebra Compiler User's Manual. Reactive Systems , Inc., Falls Church, VA. Sims, S. 1999. The Process Algebra Compiler User's Manual. Reactive Systems, Inc., Falls Church, VA."},{"key":"e_1_2_1_237_1","volume-title":"Proceedings of the 1st IEEE Conference on Formal Engineering Methods. IEEE Computer Society Press","author":"Singh H.","unstructured":"Singh , H. , Conrad , M. , and Sadeghipour , S . 1997. Test case design based on Z and the classification-tree method . In Proceedings of the 1st IEEE Conference on Formal Engineering Methods. IEEE Computer Society Press , Los Alamitos, CA, 81--90. Singh, H., Conrad, M., and Sadeghipour, S. 1997. Test case design based on Z and the classification-tree method. In Proceedings of the 1st IEEE Conference on Formal Engineering Methods. IEEE Computer Society Press, Los Alamitos, CA, 81--90."},{"key":"e_1_2_1_238_1","volume-title":"Understanding Z: A Specification Language and its Formal Semantics","author":"Spivey J. M.","unstructured":"Spivey , J. M. 1988. Understanding Z: A Specification Language and its Formal Semantics . Cambridge University Press, Cambridge , U.K. Spivey, J. M. 1988. Understanding Z: A Specification Language and its Formal Semantics. Cambridge University Press, Cambridge, U.K."},{"key":"e_1_2_1_239_1","volume-title":"The Z Notation: A Reference Manual","author":"Spivey J. M.","unstructured":"Spivey , J. M. 1992. The Z Notation: A Reference Manual , 2 nd ed. Prentice Hall International Science in Computer Science, Prentice Hall , Englewood Cliffs, NJ. Spivey, J. M. 1992. The Z Notation: A Reference Manual, 2nd ed. Prentice Hall International Science in Computer Science, Prentice Hall, Englewood Cliffs, NJ.","edition":"2"},{"key":"e_1_2_1_240_1","volume-title":"Lecture Notes in Computer Science","volume":"201","author":"Stauner T.","unstructured":"Stauner , T. , Muller , O. , and Fuchs , M . 1997. Using HYTECH to verify an automotive control system . Lecture Notes in Computer Science , vol. 201 . Springer, Berlin, Germany, 139--153. Stauner, T., Muller, O., and Fuchs, M. 1997. Using HYTECH to verify an automotive control system. Lecture Notes in Computer Science, vol. 201. Springer, Berlin, Germany, 139--153."},{"key":"e_1_2_1_241_1","series-title":"Lecture Notes in Computer Science","volume-title":"The Z Formal Specification Notation (ZUM 95)","author":"Stepney S.","unstructured":"Stepney , S. 1995. Testing as abstraction . In The Z Formal Specification Notation (ZUM 95) . Lecture Notes in Computer Science , vol. 967 . Springer, Berlin , Germany , 137--151. Stepney, S. 1995. Testing as abstraction. In The Z Formal Specification Notation (ZUM 95). Lecture Notes in Computer Science, vol. 967. Springer, Berlin, Germany, 137--151."},{"key":"e_1_2_1_242_1","volume-title":"Handbook of Logic in Computer Science.","author":"Stirling C.","unstructured":"Stirling , C. 1992. Modal and temporal logics . In Handbook of Logic in Computer Science. Vol. 2 . Oxford University Press, Oxford , U.K. , 477--563. Stirling, C. 1992. Modal and temporal logics. In Handbook of Logic in Computer Science. Vol. 2. Oxford University Press, Oxford, U.K., 477--563."},{"key":"e_1_2_1_244_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.553698"},{"key":"e_1_2_1_245_1","volume-title":"Proceedings of the IEEE International Conference on Information Reuse and Integration (IRI). 487--492","author":"Tan L.","unstructured":"Tan , L. , Kim , J. , Sokolsky , O. , and Lee , I . 2004. Model-based testing and monitoring for hybrid embedded systems . In Proceedings of the IEEE International Conference on Information Reuse and Integration (IRI). 487--492 . Tan, L., Kim, J., Sokolsky, O., and Lee, I. 2004. Model-based testing and monitoring for hybrid embedded systems. In Proceedings of the IEEE International Conference on Information Reuse and Integration (IRI). 487--492."},{"key":"e_1_2_1_246_1","volume-title":"EUROMICRO 96: Proceedings of the 22nd EUROMICRO Conference, Beyond 2000: Hardware and Software Design Strategies. 319--325","author":"Taouil-Traverson S.","unstructured":"Taouil-Traverson , S. and Vignes , S . 1996. Preliminary analysis cycle for B-method software development . In EUROMICRO 96: Proceedings of the 22nd EUROMICRO Conference, Beyond 2000: Hardware and Software Design Strategies. 319--325 . Taouil-Traverson, S. and Vignes, S. 1996. Preliminary analysis cycle for B-method software development. In EUROMICRO 96: Proceedings of the 22nd EUROMICRO Conference, Beyond 2000: Hardware and Software Design Strategies. 319--325."},{"key":"e_1_2_1_247_1","doi-asserted-by":"publisher","DOI":"10.1002\/(SICI)1097-024X(200001)30:1%3C61::AID-SPE292%3E3.0.CO;2-9"},{"key":"e_1_2_1_248_1","volume-title":"B'98: 2nd International B Conference, Recent Advances in the Development and Use of the B Method, D. Bert, Ed. Lecture Notes in Computer Science","volume":"1393","author":"Treharne H.","unstructured":"Treharne , H. , Draper , J. , and Schneider , S . 1998. Test case preparation using a prototype . In B'98: 2nd International B Conference, Recent Advances in the Development and Use of the B Method, D. Bert, Ed. Lecture Notes in Computer Science , vol. 1393 . Springer-Verlag, Berlin, Germany, 293--311. Treharne, H., Draper, J., and Schneider, S. 1998. Test case preparation using a prototype. In B'98: 2nd International B Conference, Recent Advances in the Development and Use of the B Method, D. Bert, Ed. Lecture Notes in Computer Science, vol. 1393. Springer-Verlag, Berlin, Germany, 293--311."},{"key":"e_1_2_1_249_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0169-7552(96)00017-7"},{"key":"e_1_2_1_250_1","volume-title":"Proceedings of the First European Conference on Model-Driven Software Engineering, A. Hartman and K. Dussa-Zieger, Eds. Imbuss","author":"Tretmans J.","unstructured":"Tretmans , J. and Brinksma , E . 2003. TorX: Automated Model Based Testing . In Proceedings of the First European Conference on Model-Driven Software Engineering, A. Hartman and K. Dussa-Zieger, Eds. Imbuss , M\u00f6hrendorf, Germany. 13 pages. Tretmans, J. and Brinksma, E. 2003. TorX: Automated Model Based Testing. In Proceedings of the First European Conference on Model-Driven Software Engineering, A. Hartman and K. Dussa-Zieger, Eds. Imbuss, M\u00f6hrendorf, Germany. 13 pages."},{"key":"e_1_2_1_251_1","doi-asserted-by":"publisher","DOI":"10.1145\/504087.504089"},{"key":"e_1_2_1_252_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0140-3664(99)00227-3"},{"key":"e_1_2_1_253_1","doi-asserted-by":"publisher","DOI":"10.1109\/12.559807"},{"key":"e_1_2_1_254_1","volume-title":"Proceedings of the IEEE Military Communications Conference (MILCOM","author":"Uyar M. U.","unstructured":"Uyar , M. U. and Duale , A. Y . 1999. Resolving inconsistencies in EFSM modeled specifications . In Proceedings of the IEEE Military Communications Conference (MILCOM , Atlantic City, NJ). Uyar, M. U. and Duale, A. Y. 1999. Resolving inconsistencies in EFSM modeled specifications. In Proceedings of the IEEE Military Communications Conference (MILCOM, Atlantic City, NJ)."},{"key":"e_1_2_1_255_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0950-5849(03)00062-4"},{"key":"e_1_2_1_256_1","volume-title":"Proceedings of Computer Aided Verification, 2nd International Workshop (CAV). DIMACS","volume":"3","author":"Valmari A.","year":"1990","unstructured":"Valmari , A. 1990 . A stubborn attack on the state explosion problem . In Proceedings of Computer Aided Verification, 2nd International Workshop (CAV). DIMACS , vol. 3 . AMS, Providence, RI, 25--42. Valmari, A. 1990. A stubborn attack on the state explosion problem. In Proceedings of Computer Aided Verification, 2nd International Workshop (CAV). DIMACS, vol. 3. AMS, Providence, RI, 25--42."},{"key":"e_1_2_1_257_1","doi-asserted-by":"publisher","DOI":"10.1109\/9.250509"},{"key":"e_1_2_1_258_1","volume-title":"Proceedings of the Symposium on Logic in Computer Science (LICS). IEEE Computer Society Press","author":"Vardi M.","unstructured":"Vardi , M. and Wolper , P . 1986. An automata-theoretic approach to automatic program verification . In Proceedings of the Symposium on Logic in Computer Science (LICS). IEEE Computer Society Press , Los Alamitos, CA, 332--344. Vardi, M. and Wolper, P. 1986. An automata-theoretic approach to automatic program verification. In Proceedings of the Symposium on Logic in Computer Science (LICS). IEEE Computer Society Press, Los Alamitos, CA, 332--344."},{"key":"e_1_2_1_259_1","volume-title":"Failure Diagnosis of Automata. Cybernetics","author":"Vasilevskii M. P.","unstructured":"Vasilevskii , M. P. 1973. Failure Diagnosis of Automata. Cybernetics . Plenum Publishing Corporation, New York , NY. Vasilevskii, M. P. 1973. Failure Diagnosis of Automata. Cybernetics. Plenum Publishing Corporation, New York, NY."},{"key":"e_1_2_1_260_1","volume-title":"Proceedings of the 25th Annual International Computer Software and Applications Conference (COMPSAC","author":"Vilkomir S. A.","unstructured":"Vilkomir , S. A. and Bowen , J. P . 2001. Formalization of software testing criteria using the Z notation . In Proceedings of the 25th Annual International Computer Software and Applications Conference (COMPSAC , Chicago, IL). IEEE Computer Society, Los Alamitos, CA, 351--356. Vilkomir, S. A. and Bowen, J. P. 2001. Formalization of software testing criteria using the Z notation. In Proceedings of the 25th Annual International Computer Software and Applications Conference (COMPSAC, Chicago, IL). IEEE Computer Society, Los Alamitos, CA, 351--356."},{"key":"e_1_2_1_261_1","volume-title":"Proceedings of the 2nd International Conference of B and Z Users (ZB). 291--308","author":"Vilkomir S. A.","unstructured":"Vilkomir , S. A. and Bowen , J. P . 2002. Reinforced condition\/decision coverage (RC\/DC): A new criterion for software testing . In Proceedings of the 2nd International Conference of B and Z Users (ZB). 291--308 . Vilkomir, S. A. and Bowen, J. P. 2002. Reinforced condition\/decision coverage (RC\/DC): A new criterion for software testing. In Proceedings of the 2nd International Conference of B and Z Users (ZB). 291--308."},{"key":"e_1_2_1_262_1","doi-asserted-by":"publisher","DOI":"10.1145\/186258.187153"},{"key":"e_1_2_1_263_1","volume-title":"Proceedings of the 8th SDL forum, INT","author":"von Bochmann G.","unstructured":"von Bochmann , G. , Petrenko , A. , Bellal , O. , and Marguiraga , S . 1997. Automating the process of test derivation from SDL specifications . In Proceedings of the 8th SDL forum, INT . Evry, France, 261--276. von Bochmann, G., Petrenko, A., Bellal, O., and Marguiraga, S. 1997. Automating the process of test derivation from SDL specifications. In Proceedings of the 8th SDL forum, INT. Evry, France, 261--276."},{"key":"e_1_2_1_264_1","volume-title":"Proceedings of the 2nd International Conference on Formal Engineering Methods. 36--45","author":"Waeselynck H.","unstructured":"Waeselynck , H. and Behnia , S . 1998. B model animation for external verification . In Proceedings of the 2nd International Conference on Formal Engineering Methods. 36--45 . Waeselynck, H. and Behnia, S. 1998. B model animation for external verification. In Proceedings of the 2nd International Conference on Formal Engineering Methods. 36--45."},{"key":"e_1_2_1_265_1","volume-title":"Proceedings of the 18th ACM International Conference on Software Engineering. 81--89","author":"Watanabe A.","unstructured":"Watanabe , A. and Sakamura , K . 1996. A specification-based adaptive test case generation strategy for open operating system standards . In Proceedings of the 18th ACM International Conference on Software Engineering. 81--89 . Watanabe, A. and Sakamura, K. 1996. A specification-based adaptive test case generation strategy for open operating system standards. In Proceedings of the 18th ACM International Conference on Software Engineering. 81--89."},{"key":"e_1_2_1_266_1","volume-title":"Proceedings of the Conference on Formal Approaches to Testing of Software (Brno, Czech Republic). 1--10","author":"Weyuker E. J.","year":"2002","unstructured":"Weyuker , E. J. 2002 . Thinking formally about testing without a formal specification . In Proceedings of the Conference on Formal Approaches to Testing of Software (Brno, Czech Republic). 1--10 . Weyuker, E. J. 2002. Thinking formally about testing without a formal specification. In Proceedings of the Conference on Formal Approaches to Testing of Software (Brno, Czech Republic). 1--10."},{"key":"e_1_2_1_267_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1980.234485"},{"key":"e_1_2_1_268_1","volume-title":"Protocol Specification, Testing, and Verification IX","author":"Wezeman C. D.","unstructured":"Wezeman , C. D. 1989. The CO-OP method for compositional derivation of conformance testers . In Protocol Specification, Testing, and Verification IX . Elsevier (North-Holland), Amsterdam , The Netherlands , 145--158. Wezeman, C. D. 1989. The CO-OP method for compositional derivation of conformance testers. In Protocol Specification, Testing, and Verification IX. Elsevier (North-Holland), Amsterdam, The Netherlands, 145--158."},{"key":"e_1_2_1_269_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1980.234486"},{"key":"e_1_2_1_270_1","doi-asserted-by":"publisher","DOI":"10.1002\/1099-1689(200012)10:4<229::AID-STVR213>3.0.CO;2-O"},{"key":"e_1_2_1_271_1","unstructured":"Win T. and Ernst M. 2002. Verifying distributed algorithms via dynamic analysis and theorem proving. Tech. rep. 841. MIT Laboratory for Computer Science MIT Cambridge MA.  Win T. and Ernst M. 2002. Verifying distributed algorithms via dynamic analysis and theorem proving. Tech. rep. 841. MIT Laboratory for Computer Science MIT Cambridge MA."},{"key":"e_1_2_1_272_1","doi-asserted-by":"publisher","DOI":"10.1049\/sej.1993.0027"},{"key":"e_1_2_1_273_1","doi-asserted-by":"publisher","DOI":"10.1145\/99508.99543"},{"key":"e_1_2_1_274_1","volume-title":"Protocol Specification, Testing and Verification, XIII (C-16)","author":"Yao M.","unstructured":"Yao , M. , Petrenko , A. , and von Bochmann , G. 1993. Conformance testing of protocol machines without reset . In Protocol Specification, Testing and Verification, XIII (C-16) . Elsevier (North-Holland), Amsterdam , The Netherlands , 241--256. Yao, M., Petrenko, A., and von Bochmann, G. 1993. Conformance testing of protocol machines without reset. In Protocol Specification, Testing and Verification, XIII (C-16). Elsevier (North-Holland), Amsterdam, The Netherlands, 241--256."},{"key":"e_1_2_1_275_1","first-page":"81","article-title":"On checking experiments with nondeterministic automata","volume":"6","author":"Yevtushenko N. V.","year":"1991","unstructured":"Yevtushenko , N. V. , Lebedev , A. V. , and Petrenko , A. F. 1991 . On checking experiments with nondeterministic automata . Automat. Contr. Comput. Sci. 6 , 81 -- 85 . Yevtushenko, N. V., Lebedev, A. V., and Petrenko, A. F. 1991. On checking experiments with nondeterministic automata. Automat. Contr. Comput. Sci. 6, 81--85.","journal-title":"Automat. Contr. Comput. Sci."},{"key":"e_1_2_1_276_1","doi-asserted-by":"publisher","DOI":"10.1145\/74587.74593"},{"key":"e_1_2_1_277_1","doi-asserted-by":"publisher","DOI":"10.5555\/950789.951256"}],"container-title":["ACM Computing Surveys"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1459352.1459354","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1459352.1459354","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:29:58Z","timestamp":1750253398000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1459352.1459354"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,2]]},"references-count":271,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2009,2]]}},"alternative-id":["10.1145\/1459352.1459354"],"URL":"https:\/\/doi.org\/10.1145\/1459352.1459354","relation":{},"ISSN":["0360-0300","1557-7341"],"issn-type":[{"value":"0360-0300","type":"print"},{"value":"1557-7341","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,2]]},"assertion":[{"value":"2005-01-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2008-03-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2009-02-23","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}