{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,18]],"date-time":"2025-12-18T14:02:49Z","timestamp":1766066569463},"reference-count":41,"publisher":"Sociedade Brasileira de Computacao - SB","issue":"1","license":[{"start":{"date-parts":[[2016,3,31]],"date-time":"2016-03-31T00:00:00Z","timestamp":1459382400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Softw Eng Res Dev"],"published-print":{"date-parts":[[2016,12]]},"DOI":"10.1186\/s40411-016-0027-4","type":"journal-article","created":{"date-parts":[[2016,3,31]],"date-time":"2016-03-31T11:16:41Z","timestamp":1459423001000},"update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Distinguishing extended finite state machine configurations using predicate abstraction"],"prefix":"10.5753","volume":"4","author":[{"given":"Khaled","family":"El-Fakih","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nina","family":"Yevtushenko","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marius","family":"Bozga","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Saddek","family":"Bensalem","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"3742","published-online":{"date-parts":[[2016,3,31]]},"reference":[{"issue":"9","key":"27_CR1","first-page":"1216","volume":"39","author":"WL Andrade","year":"2013","unstructured":"Andrade WL, Machado PDL (2013) Generating test cases for real-time systems based on symbolic models. IEEE TSE 39(9):1216\u20131229","journal-title":"IEEE TSE"},{"key":"27_CR2","unstructured":"Bensalem S, Bouajjani A, Loiseaux C, and Sifakis J (1992) Property-preserving simulations. In Proc. of the 4th International Conference on Computer Aided Verification- CAV \u201892, LNCS vol. 663. Springer"},{"key":"27_CR3","doi-asserted-by":"crossref","unstructured":"Bensalem S, Lakhnech Y and Owre S (1998) Computing abstractions of infinite state systems automatically and compositionally. In Proc. of Computer Aided Verification-CAV\u201998. LNCS vol. 1427, pp. 319-331. Springer","DOI":"10.1007\/BFb0028755"},{"key":"27_CR4","first-page":"109","volume-title":"Proc. of International Symposium on Software Testing and Analysis, Seattle","author":"GV Bochmann","year":"1994","unstructured":"Bochmann GV, Petrenko A (1994) Protocol testing: review of methods and relevance for software testing. In: Proc. of International Symposium on Software Testing and Analysis, Seattle., pp 109\u2013123"},{"issue":"6","key":"27_CR5","doi-asserted-by":"crossref","first-page":"693","DOI":"10.1016\/S1389-1286(00)00203-6","volume":"35","author":"C Bourhfir","year":"2001","unstructured":"Bourhfir C, Abdoulhamid E, Khendek F, Dssouli R (2001) Test cases selection from SDL specifications. Comput Netw 35(6):693\u2013708","journal-title":"Comput Netw"},{"key":"27_CR6","doi-asserted-by":"crossref","unstructured":"Bozga M, Graf S, Ober I, and Sifakis J (2004) The IF Toolset. Revised Lectures of the 4th International School on Formal Methods for the Design of Computer, Communication and Software Systems: Real Time SFM-RT 2004. LNCS vol. 3185, pp. 237-267. Springer","DOI":"10.1007\/978-3-540-30080-9_8"},{"key":"27_CR7","doi-asserted-by":"crossref","first-page":"837","DOI":"10.1016\/S0950-5849(03)00063-6","volume":"45","author":"A Cavalli","year":"2003","unstructured":"Cavalli A, Gervy C, Prokopenko S (2003) New approaches for passive testing using an extended finite state machine specification. Inf Softw Technol 45:837\u2013852","journal-title":"Inf Softw Technol"},{"key":"27_CR8","doi-asserted-by":"crossref","unstructured":"Cho H, Hachtel G, Jeong S-W, Plessier B, Schwarz E, Somenzi F (1991) Results on the interface between formal verification and ATPG. Proc. Workshop in Computer-Aided Verification Conf.(CAV\u201990), DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 3, pp. 615-627","DOI":"10.1090\/dimacs\/003\/38"},{"key":"27_CR9","doi-asserted-by":"crossref","unstructured":"Clarke E, Grumberg O, Long D (1994) Verification tools for finite-state concurrent systems. In: A Decade of Concurrency - Reflections and Perspectives. LNCS 803","DOI":"10.1007\/3-540-58043-3_19"},{"issue":"5","key":"27_CR10","doi-asserted-by":"crossref","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"EM Clarke","year":"2003","unstructured":"Clarke EM, Grumberg O, Jha S, Lu Y, Veith H (2003) Counterexample-guided abstraction refinement for symbolic model checking. J ACM 50(5):752\u2013794","journal-title":"J ACM"},{"key":"27_CR11","doi-asserted-by":"crossref","unstructured":"Clatin M, Groz R, Phalippou M, Thummel R (1995) Two approaches linking a test Generation tool with verification techniques. Proc. IFIP Eighth Int\u2019l Workshop Protocol Test Systems","DOI":"10.1007\/978-0-387-34988-6_10"},{"key":"27_CR12","unstructured":"Dams DR, Grumberg O, and Gerth R (1994) Abstract interpretation of reactive systems: abstractions preserving \u2200CTL*, \u2203CTL*, CTL*. In Proc. Of the IFIP Working Conference on Programming Concepts, Methods and Calculi"},{"key":"27_CR13","unstructured":"Das S (2003) Predicate abstraction. Ph.D. Thesis. Department of Electrical Engineering, Stanford University"},{"key":"27_CR14","doi-asserted-by":"crossref","unstructured":"El-Fakih K, Prokopenko S, Yevtushenko N, Bochmann VG (2003) Fault diagnosis in extended finite state machines. In Proc. of the 15th International Conference on Testing of Communicating Systems, LNCS vol. 2644, pp.197-210. Springer","DOI":"10.1007\/3-540-44830-6_15"},{"key":"27_CR15","doi-asserted-by":"crossref","unstructured":"El-Fakih K, Kolomeez A, Prokopenko S, Yevtushenko N (2008) Extended finite state machine based test derivation driven by user defined faults. In Proc. of the IEEE International Conference on Software Testing, Verification, and Validation- ICST 2008, Lillehammer, Norway: pp. 308-317","DOI":"10.1109\/ICST.2008.16"},{"key":"27_CR16","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1016\/S0167-6423(96)00032-9","volume":"29","author":"J-C Fernandez","year":"1996","unstructured":"Fernandez J-C, Jard C, Je\u00b4ron T, Viho C (1996) An experiment in automatic generation of test suites for protocols with verification technology. Sci Comput Program 29:123\u2013146","journal-title":"Sci Comput Program"},{"key":"27_CR17","first-page":"27","volume-title":"Proc. of the SIAM-AMS Symposium on Applied Mathematics","author":"MJ Fischer","year":"1974","unstructured":"Fischer MJ, Rabin MO (1974) Super-exponential complexity of Presburger arithmetic. In: Proc. of the SIAM-AMS Symposium on Applied Mathematics, vol 7., pp 27\u201341"},{"key":"27_CR18","first-page":"782","volume-title":"Proc. of IEEE INFOCOM\u201993","author":"A Ghedamsi","year":"1993","unstructured":"Ghedamsi A, Bochmann G, Dssouli R (1993) Multiple fault diagnosis for finite state machines. In: Proc. of IEEE INFOCOM\u201993., pp 782\u2013791"},{"key":"27_CR19","doi-asserted-by":"crossref","unstructured":"Graf S, and Saidi H (1997) Construction of abstract state graphs with PVS. In Proc. of Computer-Aided Verification-CAV\u201997. LNCS vol. 1254, pp. 72-83 Springer","DOI":"10.1007\/3-540-63166-6_10"},{"issue":"4","key":"27_CR20","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1145\/235321.235322","volume":"5","author":"D Harel","year":"1996","unstructured":"Harel D, Naamad A (1996) The STATEMATE Semantics of Statecharts. ACM Trans Softw Eng Methodol 5(4):293\u2013333","journal-title":"ACM Trans Softw Eng Methodol"},{"key":"27_CR21","doi-asserted-by":"crossref","first-page":"232","DOI":"10.1145\/964001.964021","volume-title":"Proc. of the ACM SIGPLAN-SIGACT symposium on Principles of programming languages","author":"TA Henzinger","year":"2004","unstructured":"Henzinger TA, Jhala R, Majumdar R, McMillan K (2004) Abstractions from Proofs. In: Proc. of the ACM SIGPLAN-SIGACT symposium on Principles of programming languages., pp 232\u2013244"},{"key":"27_CR22","doi-asserted-by":"crossref","unstructured":"Hierons RM, and T\u00fcrker UC (2014) Distinguishing sequences for partially specified FSMs. In Proc. of NASA Formal Methods (NFM 2014). LNCS vol. 8430, pp. 62-76. Springer","DOI":"10.1007\/978-3-319-06200-6_5"},{"key":"27_CR23","unstructured":"ITU-T (1994) Recommendation Z.100-Specification and Description Language (SDL), Geneva"},{"issue":"5","key":"27_CR24","first-page":"649","volume":"37","author":"Y Jia","year":"2011","unstructured":"Jia Y, Harman M (2011) An anaylsis and survey of the development of mutation testing. IEEE TSE 37(5):649\u2013678","journal-title":"IEEE TSE"},{"key":"27_CR25","doi-asserted-by":"crossref","unstructured":"Keum C, Kang S, Ko I-Y, Baik J, Choi Y (2006) Generating test cases for web services using extended finite state machine. In: Proc. of Testing of Communicating Systems. LNCS vol. 3964, pp. 103\u2013117. Springer","DOI":"10.1007\/11754008_7"},{"key":"27_CR26","doi-asserted-by":"crossref","unstructured":"Kushik N and Yevtushenko N (2015) Describing homing and distinguishing sequences for nondeterministic finite state machines via synchronizing automata. In Proc. of International Conference Implementation and Application of Automata. LNCS vol. 9223, pp. 188-198. Springer","DOI":"10.1007\/978-3-319-22360-5_16"},{"key":"27_CR27","first-page":"230","volume-title":"Proc. of Quality of Information and Communications Technology (QUATIC 2014)","author":"N Kushik","year":"2014","unstructured":"Kushik N, Yevtushenko N, Cavalli AR (2014) On Testing against partial non-observable specifications. In: Proc. of Quality of Information and Communications Technology (QUATIC 2014)., pp 230\u2013233"},{"issue":"3","key":"27_CR28","doi-asserted-by":"crossref","first-page":"306","DOI":"10.1109\/12.272431","volume":"43","author":"D Lee","year":"1994","unstructured":"Lee D, Yannakakis M (1994) Testing finite-state machines: state identification and verification. IEEE Trans Comput 43(3):306\u2013320","journal-title":"IEEE Trans Comput"},{"key":"27_CR29","unstructured":"Long D (1993) Model Checking, Abstraction and Compositional Verification. Ph.D. Thesis. School of Computer Science, Carnegie Mellon University, CMU-CS-93-178"},{"issue":"6","key":"27_CR30","doi-asserted-by":"crossref","first-page":"835","DOI":"10.1109\/TC.2008.15","volume":"57","author":"M Merayo","year":"2008","unstructured":"Merayo M, Nunez M, Rodriguez I (2008) Extending EFSMs to specify and test timed systems with action durations and time-outs. IEEE Trans Comput 57(6):835\u2013844","journal-title":"IEEE Trans Comput"},{"key":"27_CR31","doi-asserted-by":"crossref","unstructured":"Mounier L, Bozga M, Graf S (2002) IF-2.0: A validation environment for component-based real-time systems. In Proc. of the Int. Conf. on Computer-Aided Verification. LNCS vol. 2404, pp. 343-348. Springer","DOI":"10.1007\/3-540-45657-0_26"},{"key":"27_CR32","unstructured":"Okun V, Black PE, Yesha Y (2002) Testing with model checker: insuring fault visibility. Proc. Int. Conf. System Science, Applied Mathematics and Computer Science, and Power Eng. Systems, pp. 1351- 1356"},{"key":"27_CR33","doi-asserted-by":"crossref","unstructured":"OMG (2002) Unified Modelling Language, version 1.4. OMG Standard, Nov.","DOI":"10.1016\/S1351-4180(02)01122-4"},{"issue":"1","key":"27_CR34","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1109\/TSE.2004.1265734","volume":"30","author":"A Petrenko","year":"2004","unstructured":"Petrenko A, Boroday S, Groz R (2004) Confirming configurations in EFSM Testing. IEEE Trans Softw Eng 30(1):29\u201342","journal-title":"IEEE Trans Softw Eng"},{"key":"27_CR35","doi-asserted-by":"crossref","first-page":"1622","DOI":"10.1016\/S0140-3664(03)00116-6","volume":"26","author":"T Ramalingom","year":"2003","unstructured":"Ramalingom T, Thulasiraman K, Das A (2003) Context independent unique state identification sequences for testing communication protocols modelled as extended finite state machines. Comput Commun 26:1622\u20131633","journal-title":"Comput Commun"},{"key":"27_CR36","doi-asserted-by":"crossref","unstructured":"Rusu V, du Bousquet L, and J\u00e9ron T (2000) An approach to symbolic test generation. In Proc. Integrated Formal Methods, pp. 338-357","DOI":"10.1007\/3-540-40911-4_20"},{"issue":"4","key":"27_CR37","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1002\/stvr.374","volume":"17","author":"N Spitsyna","year":"2007","unstructured":"Spitsyna N, El-Fakih K, Yevtushenko N (2007) Studying the separability relation between finite state machines. Softw Test Verification Reliability 17(4):227\u2013241","journal-title":"Softw Test Verification Reliability"},{"key":"27_CR38","unstructured":"Starke P (1972) Abstract automata, American Elsevier, 3\u2013419"},{"key":"27_CR39","doi-asserted-by":"crossref","unstructured":"Sugeta T, Maldonado JC, Wong E (2004) Mutation testing applied to validate SDL specifications. In Proc. of the 16th International Conference on Testing of Communicating Systems. Lecture Notes in Computer Science 2978: pp. 193-208","DOI":"10.1007\/978-3-540-24704-3_13"},{"key":"27_CR40","unstructured":"Wang C-J, Koh L-S, Liu MT (1994) Protocol validation tools as test case generators, Proc. Seventh Int. Workshop Protocol Test Systems, pp. 155-170"},{"issue":"11","key":"27_CR41","doi-asserted-by":"crossref","first-page":"1505","DOI":"10.1016\/j.infsof.2009.06.005","volume":"51","author":"WE Wong","year":"2009","unstructured":"Wong WE, Restrepo A, Choi B (2009) Validation of SDL specifications using EFSM based test generation. Inf Softw Technol 51(11):1505\u20131519","journal-title":"Inf Softw Technol"}],"container-title":["Journal of Software Engineering Research and Development"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1186\/s40411-016-0027-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1186\/s40411-016-0027-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1186\/s40411-016-0027-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,6,16]],"date-time":"2022-06-16T20:11:37Z","timestamp":1655410297000},"score":1,"resource":{"primary":{"URL":"http:\/\/jserd.springeropen.com\/articles\/10.1186\/s40411-016-0027-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,3,31]]},"references-count":41,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2016,12]]}},"alternative-id":["27"],"URL":"https:\/\/doi.org\/10.1186\/s40411-016-0027-4","relation":{},"ISSN":["2195-1721"],"issn-type":[{"value":"2195-1721","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,3,31]]},"article-number":"1"}}