{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:53:03Z","timestamp":1750308783825,"version":"3.41.0"},"reference-count":27,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2006,10,1]],"date-time":"2006-10-01T00:00:00Z","timestamp":1159660800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Des. Autom. Electron. Syst."],"published-print":{"date-parts":[[2006,10]]},"abstract":"<jats:p>Verification and test are critical phases in the development of any hardware or software system. This article focuses on black box testing of the control part of hardware and software systems. Black box testing involves specification, test generation, and fault coverage. Finite state machines (FSMs) are commonly used for specifying controllers. FSMs may have shortcomings in modeling complex systems. With the introduction of X-machines, complex systems can be modeled at higher levels of abstraction. An X-machine can be converted into an FSM while preserving the level of abstraction. The fault coverage of a test sequence for an FSM specification provides a confidence level. We propose a fault coverage metric for an FSM specification based on the transition fault model, and using this metric, we derive the coverage of a test sequence. The article also presents a method which generates short test sequences that meet a specific coverage level and then extends this metric to determine the coverage of a test sequence for an FSM driven by an FSM network. We applied our FSM verification technique to a real-life FSM, namely, the fibre channel arbitrated loop port state machine, used in the field of storage area networks.<\/jats:p>","DOI":"10.1145\/1179461.1179467","type":"journal-article","created":{"date-parts":[[2007,1,16]],"date-time":"2007-01-16T19:38:29Z","timestamp":1168976309000},"page":"916-938","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Test sequence generation for controller verification and test with high coverage"],"prefix":"10.1145","volume":"11","author":[{"given":"Sezer","family":"G\u00f6ren","sequence":"first","affiliation":[{"name":"Bah\u00e7e\u015fehir University, Istanbul, Turkey"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"F. Joel","family":"Ferguson","sequence":"additional","affiliation":[{"name":"University of California Santa Cruz, Santa Cruz, CA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2006,10]]},"reference":[{"volume-title":"Proceedings of International Test Conference. 162--168","author":"Cheng K.-T.","key":"e_1_2_1_1_1"},{"volume-title":"Proceedings of the International Conference on Computer-Aided Verification. 66--78","author":"Chockler H.","key":"e_1_2_1_2_1"},{"key":"e_1_2_1_3_1","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1007\/BFb0025774","article-title":"Design and synthesis of synchronization skeletons using branching time temporal logic. In Proceedings of the Workshop on Logic of Programs","volume":"131","author":"Clarke E. M.","year":"1981","journal-title":"Lecture Notes in Computer Science"},{"volume-title":"Proceedings of the International Test Conference. 55--62","author":"Dahbura A. T.","key":"e_1_2_1_4_1"},{"key":"e_1_2_1_5_1","unstructured":"Eilenberg S. 1974. Automata Machines and Languages. Academic Press Orlando FL.]]   Eilenberg S. 1974. Automata Machines and Languages. Academic Press Orlando FL.]]"},{"key":"e_1_2_1_6_1","doi-asserted-by":"crossref","first-page":"919","DOI":"10.1109\/TVLSI.2002.808438","article-title":"Functional vector generation for sequential HDL models under an observability-based coverage metric","volume":"10","author":"Fallah F.","year":"2002","journal-title":"IEEE Trans. VLSI Syst."},{"key":"e_1_2_1_7_1","doi-asserted-by":"crossref","first-page":"760","DOI":"10.1109\/43.851991","article-title":"Symbolic optimization of interacting controllers based on redundancy identification and removal","volume":"19","author":"Ferrandi F.","year":"2000","journal-title":"IEEE Trans. Comput.-Aided Des. Integrated Circ. Syst."},{"key":"e_1_2_1_8_1","doi-asserted-by":"crossref","first-page":"652","DOI":"10.1109\/43.79502","article-title":"Test generation and verification for highly sequential circuits","volume":"10","author":"Ghosh A.","year":"1991","journal-title":"IEEE Trans. Comput.-Aided Des. Integrated Circ. Syst."},{"volume-title":"Proceedings of the International Test Conference. 406--413","author":"G\u00f6ren S.","key":"e_1_2_1_9_1"},{"volume-title":"Proceedings of the International Test Conference. 773--780","author":"G\u00f6ren S.","key":"e_1_2_1_10_1"},{"volume-title":"Proceedings of International Symposium on Switching Circuit Theory and Logic Design. 95--110","year":"1964","author":"Hennie F. C.","key":"e_1_2_1_11_1"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1049\/sej.1988.0009"},{"key":"e_1_2_1_13_1","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1002\/(SICI)1099-1689(199806)8:2<61::AID-STVR154>3.0.CO;2-W","article-title":"Specification and testing generalized machines: A presentation and a case study","volume":"8","author":"Ipate F.","year":"1998","journal-title":"Softw. Test. Verification and Reliability"},{"key":"e_1_2_1_14_1","unstructured":"Kembel R. W. and Truestedt H. L. 1997. Fibre Channel Arbitrated Loop. Northwest Learning.]]  Kembel R. W. and Truestedt H. L. 1997. Fibre Channel Arbitrated Loop. Northwest Learning.]]"},{"key":"e_1_2_1_15_1","doi-asserted-by":"crossref","first-page":"1090","DOI":"10.1109\/5.533956","article-title":"Principles and methods of testing finite state machines---A survey","volume":"84","author":"Lee D.","year":"1996","journal-title":"Proc. IEEE"},{"volume-title":"Proceedings of the Conference on Principles of Programming Languages. 97--107","year":"1859","author":"Lichtenstein O.","key":"e_1_2_1_16_1"},{"key":"e_1_2_1_17_1","unstructured":"Makar S. R. 1996. Checking experiments for scan chain latches and flip-flops. Ph.D. Dissertation Department of Electrical Engineering Stanford University.]]  Makar S. R. 1996. Checking experiments for scan chain latches and flip-flops. Ph.D. Dissertation Department of Electrical Engineering Stanford University.]]"},{"volume-title":"Automata Studies","author":"Moore E. F.","key":"e_1_2_1_18_1"},{"key":"e_1_2_1_19_1","doi-asserted-by":"crossref","unstructured":"Petrenko A. Bochmann G. V. and Yao M. 1996. On fault coverage of tests for finite state specifications. Comput. Netw. ISDN Syst. 29. (Special issue on Protocol Testing) 81--106.]] 10.1016\/S0169-7552(96)00019-0   Petrenko A. Bochmann G. V. and Yao M. 1996. On fault coverage of tests for finite state specifications. Comput. Netw. ISDN Syst. 29. (Special issue on Protocol Testing) 81--106.]] 10.1016\/S0169-7552(96)00019-0","DOI":"10.1016\/S0169-7552(96)00019-0"},{"volume-title":"Proceedings of the Conference Design Automation Conference. 341--346","author":"Pomeranz I.","key":"e_1_2_1_20_1"},{"volume-title":"Proceedings of the International Conference on Computer Design. 328--333","author":"Sentovich E. M.","key":"e_1_2_1_21_1"},{"key":"e_1_2_1_22_1","doi-asserted-by":"crossref","first-page":"1282","DOI":"10.1109\/26.156631","article-title":"Protocol conformance testing using multiple UIO sequences","volume":"40","author":"Shen Y.-N.","year":"1992","journal-title":"IEEE Trans. Commun."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.16602"},{"key":"e_1_2_1_24_1","doi-asserted-by":"crossref","unstructured":"Sun X. Shen Y. Feng C. and Lombardi. 1997. Protocol Conformance Testing Using Unique Input\/Output Sequences. World Scientific Publishing River Edge NJ.]]  Sun X. Shen Y. Feng C. and Lombardi. 1997. Protocol Conformance Testing Using Unique Input\/Output Sequences. World Scientific Publishing River Edge NJ.]]","DOI":"10.1142\/3259"},{"key":"e_1_2_1_25_1","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","article-title":"Specification and verification of concurrent systems in Cesar. In Proceedings of the International Symposium on Programming","volume":"137","author":"Queille J. P.","year":"1981","journal-title":"Lecture Notes in Computer Science"},{"volume-title":"Proceedings of the Concordia Prestigious Workshop on Communication Software Engineering.]]","author":"Uyar M.","key":"e_1_2_1_26_1"},{"key":"e_1_2_1_27_1","doi-asserted-by":"crossref","unstructured":"Yen C.-C. and Jou J.-Y. 2004. A divide-and-conquer-based algorithm for automatic simulation vector generation. IEEE Des. Test Comput. 111--120.]] 10.1109\/MDT.2004.1277903   Yen C.-C. and Jou J.-Y. 2004. A divide-and-conquer-based algorithm for automatic simulation vector generation. IEEE Des. Test Comput. 111--120.]] 10.1109\/MDT.2004.1277903","DOI":"10.1109\/MDT.2004.1277903"}],"container-title":["ACM Transactions on Design Automation of Electronic Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1179461.1179467","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1179461.1179467","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T20:22:45Z","timestamp":1750278165000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1179461.1179467"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,10]]},"references-count":27,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2006,10]]}},"alternative-id":["10.1145\/1179461.1179467"],"URL":"https:\/\/doi.org\/10.1145\/1179461.1179467","relation":{},"ISSN":["1084-4309","1557-7309"],"issn-type":[{"type":"print","value":"1084-4309"},{"type":"electronic","value":"1557-7309"}],"subject":[],"published":{"date-parts":[[2006,10]]},"assertion":[{"value":"2006-10-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}