{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T11:12:01Z","timestamp":1742382721221,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540251095"},{"type":"electronic","value":"9783540318484"}],"license":[{"start":{"date-parts":[[2005,1,1]],"date-time":"2005-01-01T00:00:00Z","timestamp":1104537600000},"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":[[2005]]},"DOI":"10.1007\/978-3-540-31848-4_9","type":"book-chapter","created":{"date-parts":[[2010,7,5]],"date-time":"2010-07-05T19:24:53Z","timestamp":1278357893000},"page":"125-139","source":"Crossref","is-referenced-by-count":23,"title":["Specifying and Generating Test Cases Using Observer Automata"],"prefix":"10.1007","author":[{"given":"Johan","family":"Blom","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anders","family":"Hessel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bengt","family":"Jonsson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paul","family":"Pettersson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"9_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"778","DOI":"10.1007\/978-3-540-45236-2_42","volume-title":"FME 2003: Formal Methods","author":"F. Bouquet","year":"2003","unstructured":"Bouquet, F., Legeard, B.: Reification of executable test scripts in formal specification-based test generation: The java card transaction mechanism case study. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805, pp. 778\u2013795. Springer, Heidelberg (2003)"},{"issue":"11","key":"9_CR2","doi-asserted-by":"publisher","first-page":"1318","DOI":"10.1109\/32.41326","volume":"SE-15","author":"L.A. Clarke","year":"1989","unstructured":"Clarke, L.A., Podgurski, A., Richardsson, D.J., Zeil, S.J.: A formal evaluation of data flow path delection criteria. IEEE Trans. on Software Engineering\u00a0SE-15(11), 1318\u20131332 (1989)","journal-title":"IEEE Trans. on Software Engineering"},{"key":"9_CR3","volume-title":"IFIP 13 th Int. Conference on Testing of Communicating Systems(TestCom 2000)","author":"L. Bousquet du","year":"2000","unstructured":"du Bousquet, L., Ramangalahy, S., Simon, S., Viho, C., Belinfante, A., de Vries, R.G.: Formal test automation: The conference protocol with tgv\/torx. In: Ural, H., Probert, R.L., von Bochmann, G. (eds.) IFIP 13 th Int. Conference on Testing of Communicating Systems(TestCom 2000). Kluwer Academic Publishers, Dordrecht (2000)"},{"doi-asserted-by":"crossref","unstructured":"du Bousquet, L., Zuanon, N.: An overview of Lutess, a specification-based tool for testing synchronous software. In: Proc. 14th IEEE Intl. Conf. on Automated SW Engineering (October 1999)","key":"9_CR4","DOI":"10.1109\/ASE.1999.802255"},{"doi-asserted-by":"crossref","unstructured":"Fernandez, J.-C., Jard, C., J\u00e9ron, T., Viho, C.: An experiment in automatic generation of test suites for protocols with verification technology. Science of Computer Programming 29 (1997)","key":"9_CR5","DOI":"10.1016\/S0167-6423(96)00032-9"},{"doi-asserted-by":"crossref","unstructured":"Friedman, G., Hartman, A., Nagin, K., Shiran, T.: Projected state machine coverage for software testing. In: Proc. ACM SIGSOFT International Symposium on Software Testing and Analysis, pp. 134\u2013143 (2002)","key":"9_CR6","DOI":"10.1145\/566172.566192"},{"issue":"1","key":"9_CR7","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/S1567-8326(01)00012-1","volume":"51","author":"S. Gnesi","year":"2002","unstructured":"Gnesi, S., Latella, D., Massink, M.: Modular semantics for a UML statechart diagrams kernel and its extension to multicharts and branching time model-checking. Journal of Logic and Algebraic Programming\u00a051(1), 43\u201375 (2002)","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/3-540-46002-0_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Havelund","year":"2002","unstructured":"Havelund, K., Rosu, G.: Synthesizing monitors for safety properties. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, pp. 324\u2013356. Springer, Heidelberg (2002)"},{"key":"9_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1007\/978-3-540-24617-6_9","volume-title":"Formal Approaches to Software Testing","author":"A. Hessel","year":"2004","unstructured":"Hessel, A., Larsen, K.G., Nielsen, B., Pettersson, P., Skou, A.: Time-Optimal Real-Time Test Case Generation using Uppaal. In: Petrenko, A., Ulrich, A. (eds.) FATES 2003. LNCS, vol.\u00a02931, pp. 136\u2013151. Springer, Heidelberg (2004)"},{"doi-asserted-by":"crossref","unstructured":"Hessel, A., Pettersson, P.: A test generation algorithm for real-time systems. To appear in Proc. of 4th Int. Conf. on Quality Software (September 2004)","key":"9_CR10","DOI":"10.1109\/QSIC.2004.1357969"},{"issue":"5","key":"9_CR11","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"SE-23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Trans. on Software Engineering\u00a0SE-23(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. on Software Engineering"},{"doi-asserted-by":"crossref","unstructured":"Hong, H.S., Cha, S.D., Lee, I., Sokolsky, O., Ural, H.: Data flow testing as model checking. In: ICSE 2003: 25th Int. Conf. on Software Enginering, pp. 232\u2013242 (May 2003)","key":"9_CR12","DOI":"10.1109\/ICSE.2003.1201203"},{"key":"9_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/3-540-46002-0_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H.S. Hong","year":"2002","unstructured":"Hong, H.S., Lee, I., Sokolsky, O., Ural, H.: A temporal logic based theory of test coverage. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, pp. 327\u2013341. Springer, Heidelberg (2002)"},{"unstructured":"ITU, Geneva: ITU-T, Z.100, Specification and Description Language (SDL) (November 1999)","key":"9_CR14"},{"issue":"3","key":"9_CR15","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1145\/229542.229545","volume":"18","author":"J. Knoop","year":"1996","unstructured":"Knoop, J., Steffen, B., Vollmer, J.: Parallelism for free: Efficient and optimal bitvector analyses for parallel programs. ACM Transactions on Programming Languages and Systems\u00a018(3), 268\u2013299 (1996)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Software Tools for Technology Transfer.\u00a01(1-2) (1997)","key":"9_CR16","DOI":"10.1007\/s100090050010"},{"doi-asserted-by":"crossref","unstructured":"Lugato, D., Bigot, C., Valot, Y.: Validation and automatic test generation on UML models: the AGATHA approach. In: Proc. 7th Int. Workshop on Formal Methods for Industrial Critical Systems (FMICS 2002). Electronic Notes in Theoretical Computer Science, vol.\u00a066 (2002)","key":"9_CR17","DOI":"10.1016\/S1571-0661(04)80402-X"},{"doi-asserted-by":"crossref","unstructured":"Marre, B., Arnould, A.: Test Sequence Generation from Lustre Descriptions: GATEL. In: Proc. 15th IEEE Intl. Conf. on Automated Software Engineering (ASE 2000), Grenoble (2000)","key":"9_CR18","DOI":"10.1109\/ASE.2000.873667"},{"doi-asserted-by":"crossref","unstructured":"Meudec, C.: ATGen: Automatic test data generation using constraint logic programming and symbolic execution. In: Proc. 1st Intl. Workshop on Automated Program Analysis, Testing, and Verification, Limerick (2000)","key":"9_CR19","DOI":"10.1002\/stvr.225"},{"key":"9_CR20","volume-title":"Advanced Compiler Design and Implementation","author":"S.S. Muchnick","year":"1997","unstructured":"Muchnick, S.S.: Advanced Compiler Design and Implementation. Morgan Kaufmann, San Francisco (1997)"},{"key":"9_CR21","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/s10009-002-0094-1","volume":"5","author":"B. Nielsen","year":"2003","unstructured":"Nielsen, B., Skou, A.: Automated test generation from timed automata. International Journal on Software Tools for Technology Transfer.\u00a05, 59\u201377 (2003)","journal-title":"International Journal on Software Tools for Technology Transfer."},{"unstructured":"Pretschner, A.: Classical search strategies for test case generation with constraint logic programming. In: Proc. Formal Approaches to Testing of Software, FATES 2001, Aalborg, Denmark, August 2001, pp. 47\u201360 (2001)","key":"9_CR22"},{"key":"9_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/3-540-40911-4_20","volume-title":"Integrated Formal Methods","author":"V. Rusu","year":"2000","unstructured":"Rusu, V., du Bousquet, L., J\u00e9ron, T.: An approach to symbolic test generation. In: Grieskamp, W., Santen, T., Stoddart, B. (eds.) IFM 2000. LNCS, vol.\u00a01945, pp. 338\u2013357. Springer, Heidelberg (2000)"},{"doi-asserted-by":"crossref","unstructured":"Schmitt, M., Ek, A., Grabowski, J., Hogrefe, D., Koch, B.: Autolink - putting sdl-based test generation into practice. In: 11th Int. Workshop on Testing of Communicating Systems (IWTCS 1998), Tomsk, Russia (September 1998)","key":"9_CR24","DOI":"10.1007\/978-0-387-35381-4_14"},{"unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proc. LICS 1986, 1st IEEE Int. Symp. on Logic in Computer Science, pp. 332\u2013344 (June 1986)","key":"9_CR25"},{"doi-asserted-by":"crossref","unstructured":"Wolper, P.: Temporal logic can be more expressive. In: Proc. 22nd Annual Symp. Foundations of Computer Science, pp. 340\u2013348 (1981)","key":"9_CR26","DOI":"10.1109\/SFCS.1981.44"}],"container-title":["Lecture Notes in Computer Science","Formal Approaches to Software Testing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-31848-4_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,22]],"date-time":"2025-02-22T16:39:52Z","timestamp":1740242392000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-31848-4_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540251095","9783540318484"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-31848-4_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}