{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T03:32:02Z","timestamp":1725852722627},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319313092"},{"type":"electronic","value":"9783319313115"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-31311-5_2","type":"book-chapter","created":{"date-parts":[[2016,4,1]],"date-time":"2016-04-01T08:37:03Z","timestamp":1459499823000},"page":"31-57","source":"Crossref","is-referenced-by-count":1,"title":["Test Reactive Systems with B\u00fcchi-Automaton-Based Temporal Requirements"],"prefix":"10.1007","author":[{"given":"Bolong","family":"Zeng","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Li","family":"Tan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,4,2]]},"reference":[{"key":"2_CR1","doi-asserted-by":"publisher","unstructured":"Bieman, J., Dreilinger, D., Lin, L.: Using fault injection to increase software test coverage. In: Proceedings of Seventh International Symposium on Software Reliability Engineering, 1996, pp. 166\u2013174 (1996). doi:\n                  10.1109\/ISSRE.1996.558776","DOI":"10.1109\/ISSRE.1996.558776"},{"key":"2_CR2","unstructured":"Dahl, O.J., Dijkstra, E.W., Hoare, C.: Structured Programming. A.P.I.C. Studies in Data Processing, vol.\u00a08. Academic Press (1972)"},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"Fraser, G., Gargantini, A.: An evaluation of model checkers for specification based test case generation. In: ICST\u201909: Proceedings of the 2009 International Conference on Software Testing Verification and Validation. IEEE Computer Society, Washington, DC, USA (2009)","DOI":"10.1109\/ICST.2009.33"},{"issue":"6","key":"2_CR4","doi-asserted-by":"crossref","first-page":"591","DOI":"10.1109\/32.87284","volume":"17","author":"S. Fujiwara","year":"1991","unstructured":"Fujiwara, S., von Bochmann, G., Khendek, F., Amalou, M., Ghedamsi, A.: Test selection based on finite state models. IEEE Trans. Softw. Eng. 17(6), 591\u2013603 (1991)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"2_CR5","first-page":"215","volume-title":"Lecture Notes in Computer Science","author":"Marie-Claude Gaudel","year":"2010","unstructured":"Gaudel, M.C.: Software testing based on formal specification. In: Borba, P., Cavalcanti, A., Sampaio, A., Woodcock, J. (eds.) Testing Techniques in Software Engineering, Second Pernambuco Summer School on Software Engineering, PSSE 2007, 3\u20137 Dec 2007, Revised Lectures. Lecture Notes in Computer Science, vol. 6153, pp. 215\u2013242. Springer, Berlin (2010)"},{"key":"2_CR6","first-page":"1","volume-title":"Tests and Proofs","author":"Marie-Claude Gaudel","year":"2011","unstructured":"Gaudel, M.C.: Checking models, proving programs, and testing systems. In: Gogolla, M., Wolff, B. (eds.) TAP 2011 Proceedings. Lecture Notes in Computer Science, vol. 6706, pp. 1\u201313. Springer, Berlin (2011)"},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Protocol Specification Testing and Verification. Chapman & Hall (1995)","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"Hartman, A., Nagin, K.: The agedis tools for model based testing. In: ISSTA\u201904: Proceedings of the ACM\/SIGSOFT International Symposium on Software Testing and Analysis. ACM (2004)","DOI":"10.1145\/1007512.1007529"},{"issue":"2","key":"2_CR9","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1459352.1459354","volume":"41","author":"Robert M. Hierons","year":"2009","unstructured":"Hierons, R.M., Bogdanov, K., Bowen, J.P., Cleaveland, R., Derrick, J., Dick, J., Gheorghe, M., Harman, M., Kapoor, K., Krause, P., L\u00fcttgen, G., Simons, A.J.H., Vilkomir, S., Woodward, M.R., Zedan, H.: Using formal specifications to support testing. ACM Comput. Surv. 41(2), 9:1\u20139:76 (2009)","journal-title":"ACM Computing Surveys"},{"issue":"5","key":"2_CR10","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23, 279 (1997)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"2_CR11","doi-asserted-by":"crossref","first-page":"327","DOI":"10.1007\/3-540-46002-0_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Hyoung Seok Hong","year":"2002","unstructured":"Hong, H.S., Lee, I., Sokolsky, O., Ural, H.: A temporal logic based theory of test coverage and generation. In: TACAS\u201902 (2002)"},{"key":"2_CR12","volume-title":"Software Testing: A Craftsman\u2019s Approach","author":"PC Jorgensen","year":"1995","unstructured":"Jorgensen, P.C.: Software Testing: A Craftsman\u2019s Approach, 1st edn. CRC Press Inc., Boca Raton, FL, USA (1995)","edition":"1"},{"key":"2_CR13","unstructured":"Joseph, S.: Fault-Injection through Model Checking via Naive Assumptions about State Machine Synchrony Semantics. Master\u2019s thesis, West Virginia University, Morgantown, West Virginia (1998)"},{"issue":"4","key":"2_CR14","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1007\/s100090050045","volume":"2","author":"Moataz Kamel","year":"2000","unstructured":"Kamel, M., Leue, S.: Formalization and validation of the general inter-ORB protocol (GIOP) using PROMELA and SPIN. Int. J. Softw. Tools Technol. Transf. (STTT) 2(4), 394\u2013409 (2000)","journal-title":"International Journal on Software Tools for Technology Transfer (STTT)"},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"Knight, J.: Safety critical systems: challenges and directions. In: Proceedings of the 24rd International Conference on Software Engineering. ICSE 2002, pp. 547\u2013550 (2002)","DOI":"10.1145\/581339.581406"},{"key":"2_CR16","unstructured":"MathWorks: Simulink design verifier (2015). \n                  http:\/\/www.mathworks.com\/products\/sldesignverifier\/"},{"key":"2_CR17","unstructured":"MathWorks Inc.: Stateflow examples (2015). \n                  http:\/\/www.mathworks.com\/help\/stateflow\/examples.html"},{"key":"2_CR18","doi-asserted-by":"crossref","unstructured":"Meinke, K., Sindhu, M.A.: Incremental learning-based testing for reactive systems. In: Tests and Proofs, pp. 134\u2013151. Springer (2011)","DOI":"10.1007\/978-3-642-21768-5_11"},{"key":"2_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-642-10373-5_13","volume-title":"Formal Methods and Software Engineering","author":"A Platzer","year":"2009","unstructured":"Platzer, A., Quesel, J.D.: European train control system: a case study in formal verification. In: Breitman, K., Cavalcanti, A. (eds.) Formal Methods and Software Engineering. Lecture Notes in Computer Science, vol. 5885, pp. 246\u2013265. Springer, Berlin (2009)"},{"key":"2_CR20","unstructured":"Reactive Systems Inc.: Testing and validation of simulink models with reactis (2010). \n                  http:\/\/www.reactive-systems.com\/"},{"key":"2_CR21","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1007\/978-3-642-21768-5_13","volume-title":"Tests and Proofs","author":"Li Tan","year":"2011","unstructured":"Tan, L.: State coverage metrics for specification-based testing with B\u00fcchi automata. In: 5th International Conference on Tests and Proofs, Lecture Notes in Computer Science. Springer, Zurich, Switzerland (2011)"},{"key":"2_CR22","unstructured":"Tan, L., Sokolsky, O., Lee, I.: Specification-based Testing with Linear Temporal Logic. In: the proceedings of IEEE Internation Conference on Information Reuse and Integration (IRI\u201904). IEEE Society (2004)"},{"key":"2_CR23","doi-asserted-by":"crossref","unstructured":"Tan, L., Zeng, B.: Specification-based testing with Buchi automata: transition coverage criteria and property refinement. In: International Conference on Information Reuse and Integration. IEEE (2014)","DOI":"10.1109\/IRI.2014.7051871"},{"key":"2_CR24","doi-asserted-by":"crossref","unstructured":"Tretmans, J.: Model based testing with labelled transition systems. In: Formal methods and testing, pp. 1\u201338. Springer (2008)","DOI":"10.1007\/978-3-540-78917-8_1"},{"key":"2_CR25","doi-asserted-by":"crossref","unstructured":"Tsay, Y.K., Chen, Y.F., Tsai, M.H., Wu, K.N., Chan, W.C.: GOAL: A Graphical Tool for Manipulating B\u00fcchi Automata and Temporal Formulae. In: 13th Tools and Algorithms for the Construction and Analysis of Systems, vol. 02, pp. 466\u2013471. Springer (2007)","DOI":"10.1007\/978-3-540-71209-1_35"},{"issue":"3","key":"2_CR26","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1109\/MS.2009.67","volume":"26","author":"J Yoo","year":"2009","unstructured":"Yoo, J., Jee, E., Cha, S.: Formal modeling and verification of safety-critical software. IEEE Softw. 26(3), 42\u201349 (2009)","journal-title":"IEEE Softw."},{"key":"2_CR27","unstructured":"Young, M., Pezze, M.: Software Testing and Analysis: Process, Principles and Techniques. Wiley (2005)"},{"key":"2_CR28","unstructured":"Zeng, B., Tan, L.: Test criteria for model-checking-assisted test case generation: a computational study. In: International Conference on Information Reuse and Integration. IEEE (2012)"},{"issue":"5","key":"2_CR29","doi-asserted-by":"publisher","first-page":"823","DOI":"10.1007\/s10796-013-9424-y","volume":"16","author":"B Zeng","year":"2014","unstructured":"Zeng, B., Tan, L.: A unified framework for evaluating test criteria in model-checking-assisted test case generation. Inf. Syst. Front. 16(5), 823\u2013834 (2014)","journal-title":"Inf. Syst. Front."},{"key":"2_CR30","doi-asserted-by":"crossref","unstructured":"Zeng, B., Tan, L.: Test reactive systems with buchi automata: acceptance condition coverage criteria and performance evaluation. In: 2015 IEEE International Conference on Information Reuse and Integration, IRI 2015, San Francisco, CA, USA, August 13\u201315, pp. 380\u2013387 (2015)","DOI":"10.1109\/IRI.2015.64"},{"key":"2_CR31","unstructured":"Zeng, B., Tan, L.: Testing with buchi automata: transition coverage metrics, performance analysis, and property refinement. Advances in Intelligent Systems and Computing (2015)"}],"container-title":["Advances in Intelligent Systems and Computing","Theoretical Information Reuse and Integration"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-31311-5_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T23:01:14Z","timestamp":1559430074000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-31311-5_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319313092","9783319313115"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-31311-5_2","relation":{},"ISSN":["2194-5357","2194-5365"],"issn-type":[{"type":"print","value":"2194-5357"},{"type":"electronic","value":"2194-5365"}],"subject":[],"published":{"date-parts":[[2016]]}}}