{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T05:55:22Z","timestamp":1725602122626},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642244308"},{"type":"electronic","value":"9783642244315"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-24431-5_10","type":"book-chapter","created":{"date-parts":[[2011,8,23]],"date-time":"2011-08-23T22:29:46Z","timestamp":1314138586000},"page":"117-133","source":"Crossref","is-referenced-by-count":3,"title":["Experiences with Formal Engineering: Model-Based Specification, Implementation and Testing of a Software Bus at Neopost."],"prefix":"10.1007","author":[{"given":"Marten","family":"Sijtema","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mari\u00eblle I. A.","family":"Stoelinga","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Axel","family":"Belinfante","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lawrence","family":"Marinelli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"10_CR1","unstructured":"Conformiq webpage (April 2011), http:\/\/www.conformiq.com\/"},{"key":"10_CR2","unstructured":"Jararaca manual, http:\/\/fmt.cs.utwente.nl\/tools\/torx\/jararaca.1.html"},{"key":"10_CR3","unstructured":"JTorX webpage (August 2009), http:\/\/fmt.ewi.utwente.nl\/tools\/jtorx\/"},{"key":"10_CR4","unstructured":"mCRL2 toolkit webpage (September 2009), http:\/\/www.mcrl2.org\/"},{"key":"10_CR5","unstructured":"Neopost Inc. webpage (August 2009), http:\/\/www.neopost.com\/"},{"key":"10_CR6","unstructured":"Quasimodo webpage (August 2011), http:\/\/www.quasimodo.aau.dk\/"},{"key":"10_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/978-3-642-12002-2_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Belinfante","year":"2010","unstructured":"Belinfante, A.: JTorX: A tool for on-line model-driven test derivation and execution. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 266\u2013270. Springer, Heidelberg (2010)"},{"key":"10_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1007\/11498490_18","volume-title":"Model-Based Testing of Reactive Systems","author":"A. Belinfante","year":"2005","unstructured":"Belinfante, A., Frantzen, L., Schallhart, C.: Tools for test case generation. In: Broy, M., Jonsson, B., Katoen, J.-P., Leucker, M., Pretschner, A. (eds.) Model-Based Testing of Reactive Systems. LNCS, vol.\u00a03472, pp. 391\u2013438. Springer, Heidelberg (2005)"},{"key":"10_CR9","first-page":"179","volume-title":"IWTCS 1999","author":"A. Belinfante","year":"1999","unstructured":"Belinfante, A., et al.: Formal test automation: A simple experiment. In: Csopaki, G., Dibuz, S., Tarnay, K. (eds.) IWTCS 1999, pp. 179\u2013196. Kluwer, Dordrecht (1999)"},{"key":"10_CR10","volume-title":"Proceedings of the CWI Symposium on Mathematics and Computer Science","author":"J.A. Bergstra","year":"1985","unstructured":"Bergstra, J.A., Klop, J.W.: Algebra of communicating processes. In: de Bakker, J.W., Hazewinkel, M., Lenstra, J.K. (eds.) Proceedings of the CWI Symposium on Mathematics and Computer Science. CWI, Amsterdam (1985)"},{"key":"10_CR11","unstructured":"Blom, S.C.C., van de Pol, J.C., Weber, M.: Bridging the gap between enumerative and symbolic model checkers. Technical Report TR-CTIT-09-30, Centre for Telematics and Information Technology, University of Twente, Enschede (2009)"},{"key":"10_CR12","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1145\/1450058.1450089","volume-title":"Proceedings of the 7th ACM International Conference on Embedded Software","author":"H.C. Bohnenkamp","year":"2008","unstructured":"Bohnenkamp, H.C., Stoelinga, M.I.A.: Quantitative testing. In: Proceedings of the 7th ACM International Conference on Embedded Software, pp. 227\u2013236. ACM, New York (2008)"},{"key":"10_CR13","unstructured":"Brand\u00e1n Briones, L.: Theories for Model-based Testing: Real-time and Coverage. Ph.D. thesis, University of Twente (March 2007)"},{"key":"10_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1007\/11901914_30","volume-title":"Automated Technology for Verification and Analysis","author":"E. Brinksma","year":"2006","unstructured":"Brinksma, E., Briones, L.B., Stoelinga, M.I.A.: A semantic framework for test coverage. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol.\u00a04218, pp. 399\u2013414. Springer, Heidelberg (2006)"},{"key":"10_CR15","series-title":"Lecture Notes in Computer Science","volume-title":"Formal Methods for Industrial Critical Systems","year":"2009","unstructured":"Cofer, D., Fantechi, A. (eds.): FMICS 2008. LNCS, vol.\u00a05596. Springer, Heidelberg (2009)"},{"key":"10_CR16","first-page":"61","volume-title":"ICST","author":"A. David","year":"2009","unstructured":"David, A., Larsen, K.G., Li, S., Nielsen, B.: Timed testing under partial observability. In: ICST, pp. 61\u201370. IEEE Computer Society, Los Alamitos (2009)"},{"key":"10_CR17","doi-asserted-by":"crossref","unstructured":"Ferrari, A., Grasso, D., Magnani, G., Fantechi, A., Tempestini, M.: The metr\u00f4 rio atp case study. In: Kowalewski, S., Roveri, M. (eds.) [27], pp. 1\u201316","DOI":"10.1007\/978-3-642-15898-8_1"},{"key":"10_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/11940197_3","volume-title":"Formal Approaches to Software Testing and Runtime Verification","author":"L. Frantzen","year":"2006","unstructured":"Frantzen, L., Tretmans, J., Willemse, T.A.C.: A symbolic framework for model-based testing. In: Havelund, K., N\u00fa\u00f1ez, M., Ro\u015fu, G., Wolff, B. (eds.) FATES 2006 and RV 2006. LNCS, vol.\u00a04262, pp. 40\u201354. Springer, Heidelberg (2006)"},{"issue":"3","key":"10_CR19","doi-asserted-by":"crossref","first-page":"314","DOI":"10.1007\/s100090100044","volume":"3","author":"H. Garavel","year":"2001","unstructured":"Garavel, H., Viho, C., Zendri, M.: System design of a cc-numa multiprocessor architecture using formal specification, model-checking, co-simulation, and test generation. STTT\u00a03(3), 314\u2013331 (2001)","journal-title":"STTT"},{"key":"10_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/978-3-540-73368-3_18","volume-title":"Computer Aided Verification","author":"H. Garavel","year":"2007","unstructured":"Garavel, H., et al.: Cadp 2006: A toolbox for the construction and analysis of distributed processes. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 158\u2013163. Springer, Heidelberg (2007)"},{"key":"10_CR21","unstructured":"GraphML work group: GraphML file format, http:\/\/graphml.graphdrawing.org\/"},{"key":"10_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-642-05031-2_7","volume-title":"Testing of Software and Communication Systems","author":"W. Grieskamp","year":"2009","unstructured":"Grieskamp, W., Qu, X., Wei, X., Kicillof, N., Cohen, M.B.: Interaction coverage meets path coverage by SMT constraint solving. In: N\u00fa\u00f1ez, M., Baker, P., Merayo, M.G. (eds.) TESTCOM 2009. LNCS, vol.\u00a05826, pp. 97\u2013112. Springer, Heidelberg (2009)"},{"key":"10_CR23","unstructured":"Groote, J.F., et al.: The mCRL2 toolset. In: Proc. International Workshop on Advanced Software Development Tools and Techniques, WASDeTT 2008 (2008)"},{"issue":"1-2","key":"10_CR24","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/s11334-009-0116-1","volume":"6","author":"H.H. Hansen","year":"2010","unstructured":"Hansen, H.H., Ketema, J., Luttik, S.P., Mousavi, M.R., van de Pol, J.C.: Towards model checking executable uml specifications in mcrl2. Innovations in Systems and Software Engineering\u00a06(1-2), 83\u201390 (2010)","journal-title":"Innovations in Systems and Software Engineering"},{"key":"10_CR25","unstructured":"Hartman, A.: Model based test generation tools survey. Tech. rep., Centre for Telematics and Information Technology, University of Twente (2009)"},{"key":"10_CR26","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1145\/1013886.1007529","volume":"29","author":"A. Hartman","year":"2004","unstructured":"Hartman, A., Nagin, K.: The agedis tools for model based testing. SIGSOFT Softw. Eng. Notes\u00a029, 129\u2013132 (2004)","journal-title":"SIGSOFT Softw. Eng. Notes"},{"key":"10_CR27","series-title":"Lecture Notes in Computer Science","volume-title":"Formal Methods for Industrial Critical Systems","year":"2010","unstructured":"Kowalewski, S., Roveri, M. (eds.): FMICS 2010. LNCS, vol.\u00a06371. Springer, Heidelberg (2010)"},{"key":"10_CR28","unstructured":"Larsen, K.G., Mikucionis, M., Nielsen, B.: Online testing of real-time systems using uppaal: Status and future work. In: Perspectives of Model-Based Testing. Dagstuhl Seminar Proceedings, vol.\u00a004371 (2004)"},{"key":"10_CR29","doi-asserted-by":"crossref","unstructured":"Leveson, N.G.: Experiences in designing and using formal specification languages for embedded control software. In: Lynch, N.A., Krogh, B.H. (eds.) [30], p. 3","DOI":"10.1007\/3-540-46430-1_2"},{"key":"10_CR30","series-title":"Lecture Notes in Computer Science","volume-title":"Hybrid Systems: Computation and Control","year":"2000","unstructured":"Lynch, N.A., Krogh, B.H. (eds.): HSCC 2000. LNCS, vol.\u00a01790. Springer, Heidelberg (2000)"},{"issue":"1","key":"10_CR31","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1049\/sej.1986.0003","volume":"1","author":"P.E. Rook","year":"1986","unstructured":"Rook, P.E.: Controlling software projects. IEE Software Engineering Journal\u00a01(1), 7\u201316 (1986)","journal-title":"IEE Software Engineering Journal"},{"key":"10_CR32","series-title":"NATO Science for Peace and Security Series - D: Information and Communication Security","volume-title":"Software and Systems Safety: Specification and Verification","author":"M. Timmer","year":"2011","unstructured":"Timmer, M., Brinksma, E., Stoelinga, M.: Model-based testing. In: Software and Systems Safety: Specification and Verification. NATO Science for Peace and Security Series - D: Information and Communication Security. IOS Press, Amsterdam (2011)"},{"key":"10_CR33","unstructured":"Tretmans, J., Brinksma, H.: TorX: Automated model-based testing. In: Hartman, A., Dussa-Ziegler, K. (eds.) First European Conference on Model-Driven Software Engineering, Nuremberg, Germany, pp. 31\u201343 (December 2003)"},{"key":"10_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-540-78917-8_2","volume-title":"Formal Methods and Testing","author":"M. Veanes","year":"2008","unstructured":"Veanes, M., Campbell, C., Grieskamp, W., Schulte, W., Tillmann, N., Nachmanson, L.: Model-based testing of object-oriented reactive systems with spec explorer. In: Hierons, R.M., Bowen, J.P., Harman, M. (eds.) FORTEST. LNCS, vol.\u00a04949, pp. 39\u201376. Springer, Heidelberg (2008)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Industrial Critical Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-24431-5_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,22]],"date-time":"2020-06-22T11:41:10Z","timestamp":1592826070000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-24431-5_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642244308","9783642244315"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-24431-5_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}