{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,11]],"date-time":"2026-05-11T11:20:51Z","timestamp":1778498451394,"version":"3.51.4"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030034269","type":"print"},{"value":"9783030034276","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-030-03427-6_11","type":"book-chapter","created":{"date-parts":[[2018,10,29]],"date-time":"2018-10-29T16:54:48Z","timestamp":1540832088000},"page":"82-103","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["Model-Based Testing for Avionic Systems Proven Benefits and Further Challenges"],"prefix":"10.1007","author":[{"given":"Jan","family":"Peleska","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J\u00f6rg","family":"Brauer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wen-ling","family":"Huang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,10,30]]},"reference":[{"key":"11_CR1","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/j.scico.2017.07.002","volume":"162","author":"HLS Araujo","year":"2018","unstructured":"Araujo, H.L.S., Carvalho, G., Mohaqeqi, M., Mousavi, M.R., Sampaio, A.: Sound conformance testing for cyber-physical systems: theory and implementation. Sci. Comput. Program. 162, 35\u201354 (2018). https:\/\/doi.org\/10.1016\/j.scico.2017.07.002","journal-title":"Sci. Comput. Program."},{"key":"11_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-540-74984-4_2","volume-title":"SDL 2007: Design for Dependable Systems","author":"M Banci","year":"2007","unstructured":"Banci, M., Fantechi, A., Gnesi, S., Lombardi, G.: Model driven development and code generation: an automotive case study. In: Gaudin, E., Najm, E., Reed, R. (eds.) SDL 2007. LNCS, vol. 4745, pp. 19\u201334. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74984-4_2"},{"key":"11_CR3","doi-asserted-by":"crossref","unstructured":"Biere, A., Heljanko, K., Junttila, T., Latvala, T., Schuppan, V.: Linear encodings of bounded LTL model checking. Log. Methods Comput. Sci. 2(5) (2006). arXiv:cs\/0611029","DOI":"10.2168\/LMCS-2(5:5)2006"},{"key":"11_CR4","series-title":"IFIP Advances in Information and Communication Technology","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/978-0-387-35516-0_14","volume-title":"Testing of Communicating Systems","author":"L Du Bousquet","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., v. Bochmann, G. (eds.) Testing of Communicating Systems. IAICT, vol. 48, pp. 221\u2013228. Springer, Boston, MA (2000). https:\/\/doi.org\/10.1007\/978-0-387-35516-0_14"},{"key":"11_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1007\/978-3-642-34691-0_3","volume-title":"Testing Software and Systems","author":"J Brauer","year":"2012","unstructured":"Brauer, J., Peleska, J., Schulze, U.: Efficient and trustworthy tool qualification for model-based testing tools. In: Nielsen, B., Weise, C. (eds.) ICTSS 2012. LNCS, vol. 7641, pp. 8\u201323. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-34691-0_3"},{"key":"11_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"657","DOI":"10.1007\/978-3-319-95582-7_40","volume-title":"Formal Methods","author":"J Brauer","year":"2018","unstructured":"Brauer, J., Schulze, U.: Model-based testing for avionics systems. In: Havelund, K., Peleska, J., Roscoe, B., de Vink, E. (eds.) FM 2018. LNCS, vol. 10951, pp. 657\u2013661. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-95582-7_40"},{"key":"11_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-3-540-87603-8_8","volume-title":"Abstract State Machines, B and Z","author":"A Cavarra","year":"2008","unstructured":"Cavarra, A.: Data flow analysis and testing of abstract state machines. In: B\u00f6rger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol. 5238, pp. 85\u201397. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-87603-8_8"},{"issue":"3","key":"11_CR8","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1109\/TSE.1978.231496","volume":"SE\u20134","author":"TS Chow","year":"1978","unstructured":"Chow, T.S.: Testing software design modeled by finite-state machines. IEEE Trans. Softw. Eng. SE\u20134(3), 178\u2013186 (1978)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"11_CR9","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)"},{"key":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-540-78917-8_3","volume-title":"Formal Methods and Testing","author":"A Hessel","year":"2008","unstructured":"Hessel, A., Larsen, K.G., Mikucionis, M., Nielsen, B., Pettersson, P., Skou, A.: Testing real-time systems using UPPAAL. In: Hierons, R.M., Bowen, J.P., Harman, M. (eds.) Formal Methods and Testing. LNCS, vol. 4949, pp. 77\u2013117. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78917-8_3"},{"key":"11_CR11","unstructured":"Hou, Z., San\u00e1n, D., Tiu, A., Liu, Y.: A formal model for the SPARCv8 ISA and a proof of non-interference for the LEON3 processor. Archive of Formal Proofs 2016 (2016). https:\/\/www.isa-afp.org\/entries\/SPARCv8.shtml"},{"issue":"3","key":"11_CR12","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/s10009-014-0356-8","volume":"18","author":"W Huang","year":"2016","unstructured":"Huang, W., Peleska, J.: Complete model-based equivalence class testing. Softw. Tools Technol. Transfer 18(3), 265\u2013283 (2016). https:\/\/doi.org\/10.1007\/s10009-014-0356-8","journal-title":"Softw. Tools Technol. Transfer"},{"issue":"2","key":"11_CR13","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/s00165-016-0402-2","volume":"29","author":"W Huang","year":"2017","unstructured":"Huang, W., Peleska, J.: Complete model-based equivalence class testing for nondeterministic systems. Formal Aspects of Comput. 29(2), 335\u2013364 (2017). https:\/\/doi.org\/10.1007\/s00165-016-0402-2","journal-title":"Formal Aspects of Comput."},{"key":"11_CR14","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/s10009-017-0479-9","volume":"20","author":"W Huang","year":"2017","unstructured":"Huang, W., Peleska, J.: Model-based testing strategies and their (in)dependence on syntactic model representations. Int. J. Softw. Tools Technol. Transf. 20, 441\u2013465 (2017). https:\/\/doi.org\/10.1007\/s10009-017-0479-9","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"11_CR15","doi-asserted-by":"publisher","unstructured":"H\u00fcbner, F., Huang, W., Peleska, J.: Experimental evaluation of a novel equivalence class partition testing strategy. Softw. Syst. Model. (2017). https:\/\/doi.org\/10.1007\/s10270-017-0595-8","DOI":"10.1007\/s10270-017-0595-8"},{"key":"11_CR16","unstructured":"Jensen, H.E., Larsen, K.G., Skou, A.: Modelling and analysis of a collision avoidance protocol using spin and UPPAAL. In: Gr\u00e9goire, J., Holzmann, G.J., Peled, D.A. (eds.) The Spin Verification System, Proceedings of a DIMACS Workshop, New Brunswick, New Jersey, USA, August 1996. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 32, pp. 33\u201350. DIMACS\/AMS (1996). http:\/\/dimacs.rutgers.edu\/Volumes\/Vol32.html"},{"key":"11_CR17","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-540-88479-8_8","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation","author":"D K\u00e4stner","year":"2008","unstructured":"K\u00e4stner, D., et al.: Timing validation of automotive software. In: Margaria, T., Steffen, B. (eds.) ISoLA 2008. CCIS, vol. 17, pp. 93\u2013107. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-88479-8_8"},{"key":"11_CR18","volume-title":"Introduction to Combinatorial Testing","author":"DR Kuhn","year":"2013","unstructured":"Kuhn, D.R., Kacker, R.N., Lei, Y.: Introduction to Combinatorial Testing. CRC Press, Boca Raton (2013)"},{"key":"11_CR19","unstructured":"Larsen, K.G., Mikucionis, M., Nielsen, B., Skou, A.: Testing real-time embedded software using UPPAAL-TRON: an industrial case study. In: Proceedings of the 5th ACM International Conference on Embedded Software, EMSOFT 2005, pp. 299\u2013306. ACM, New York (2005). http:\/\/doi.acm.org\/10.1145\/1086228.1086283"},{"key":"11_CR20","unstructured":"Lee, J., Kang, S., Lee, D.: A survey on software product line testing. In: Proceedings of the 16th International Software Product Line Conference, SPLC 2012, vol. 1, pp. 31\u201340. ACM, New York (2012). http:\/\/doi.acm.org\/10.1145\/2362536.2362545"},{"key":"11_CR21","doi-asserted-by":"publisher","unstructured":"Mohacsi, S., Felderer, M., Beer, A.: A case study on the efficiency of model-based testing at the European space agency. In: 8th IEEE International Conference on Software Testing, Verification and Validation, ICST 2015, Graz, Austria, 13\u201317 April 2015, pp. 1\u20132. IEEE Computer Society (2015). https:\/\/doi.org\/10.1109\/ICST.2015.7102618","DOI":"10.1109\/ICST.2015.7102618"},{"key":"11_CR22","doi-asserted-by":"publisher","unstructured":"Mohacsi, S., Felderer, M., Beer, A.: Estimating the cost and benefit of model-based testing: a decision support procedure for the application of model-based testing in industry. In: 41st Euromicro Conference on Software Engineering and Advanced Applications, EUROMICRO-SEAA 2015, Madeira, Portugal, 26\u201328 August 2015, pp. 382\u2013389. IEEE Computer Society (2015). https:\/\/doi.org\/10.1109\/SEAA.2015.18","DOI":"10.1109\/SEAA.2015.18"},{"key":"11_CR23","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/S0065-2458(10)80002-6","volume":"80","author":"ACD Neto","year":"2010","unstructured":"Neto, A.C.D., Travassos, G.H.: A picture from the model-based testing area: concepts, techniques, and challenges. Adv. Comput. 80, 45\u2013120 (2010). https:\/\/doi.org\/10.1016\/S0065-2458(10)80002-6","journal-title":"Adv. Comput."},{"key":"11_CR24","unstructured":"Object Management Group: OMG Systems Modeling Language (OMG SysML), Version 1.4. Technical report, Object Management Group (2015). http:\/\/www.omg.org\/spec\/SysML\/1.4"},{"key":"11_CR25","doi-asserted-by":"crossref","unstructured":"Peleska, J.: Industrial-strength model-based testing - state of the art and current challenges. In: Petrenko, A.K., Schlingloff, H. (eds.) Proceedings Eighth Workshop on Model-Based Testing, Rome, Italy, 17th March 2013. Electronic Proceedings in Theoretical Computer Science, vol. 111, pp. 3\u201328. Open Publishing Association (2013)","DOI":"10.4204\/EPTCS.111.1"},{"key":"11_CR26","doi-asserted-by":"publisher","unstructured":"Peleska, J.: Model-based avionic systems testing for the airbus family. In: 23rd IEEE European Test Symposium, ETS 2018, Bremen, Germany, 28 May\u20131 June 2018, pp. 1\u201310. IEEE (2018). https:\/\/doi.org\/10.1109\/ETS.2018.8400703","DOI":"10.1109\/ETS.2018.8400703"},{"key":"11_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-319-33951-1_3","volume-title":"Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification","author":"J Peleska","year":"2016","unstructured":"Peleska, J., Huang, W., H\u00fcbner, F.: A novel approach to HW\/SW integration testing of route-based interlocking system controllers. In: Lecomte, T., Pinger, R., Romanovsky, A. (eds.) RSSRail 2016. LNCS, vol. 9707, pp. 32\u201349. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-33951-1_3"},{"key":"11_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/978-3-642-20398-5_22","volume-title":"NASA Formal Methods","author":"J Peleska","year":"2011","unstructured":"Peleska, J., Vorobev, E., Lapschies, F.: Automated test case generation with SMT-solving and abstract interpretation. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 298\u2013312. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-20398-5_22"},{"key":"11_CR29","doi-asserted-by":"publisher","unstructured":"Petrenko, A.: Checking experiments for symbolic input\/output finite state machines. In: Ninth IEEE International Conference on Software Testing, Verification and Validation Workshops, ICST Workshops 2016, Chicago, IL, USA, 11\u201315 April 2016, pp. 229\u2013237. IEEE Computer Society (2016). https:\/\/doi.org\/10.1109\/ICSTW.2016.9","DOI":"10.1109\/ICSTW.2016.9"},{"issue":"4","key":"11_CR30","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/s10009-012-0240-3","volume":"14","author":"A Petrenko","year":"2012","unstructured":"Petrenko, A., Simao, A., Maldonado, J.C.: Model-based testing of software and systems: recent advances and challenges. Int. J. Softw. Tools Technol. Transf. 14(4), 383\u2013386 (2012). https:\/\/doi.org\/10.1007\/s10009-012-0240-3","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"11_CR31","unstructured":"RTCA SC-205\/EUROCAE WG-71: Software Considerations in Airborne Systems and Equipment Certification. Technical report, RTCA\/DO-178C, RTCA Inc, 1140 Connecticut Avenue, N.W., Suite 1020, Washington, D.C. 20036, December 2011"},{"issue":"5","key":"11_CR32","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/BF01211865","volume":"6","author":"AP Sistla","year":"1994","unstructured":"Sistla, A.P.: Safety, liveness and fairness in temporal logic. Formal Aspects Comput. 6(5), 495\u2013511 (1994)","journal-title":"Formal Aspects Comput."},{"issue":"5","key":"11_CR33","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1002\/stvr.456","volume":"22","author":"M Utting","year":"2012","unstructured":"Utting, M., Pretschner, A., Legeard, B.: A taxonomy of model-based testing approaches. Softw. Test. Verif. Reliab. 22(5), 297\u2013312 (2012). https:\/\/doi.org\/10.1002\/stvr.456","journal-title":"Softw. Test. Verif. Reliab."},{"key":"11_CR34","first-page":"98","volume":"4","author":"MP Vasilevskii","year":"1973","unstructured":"Vasilevskii, M.P.: Failure diagnosis of automata. Kibernetika (Transl.) 4, 98\u2013108 (1973)","journal-title":"Kibernetika (Transl.)"},{"key":"11_CR35","unstructured":"Wei\u00dfleder, S.: Test models and coverage criteria for automatic model-based test generation with UML state machines. Ph.D. thesis, Humboldt University of Berlin (2010). http:\/\/d-nb.info\/1011308983"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-03427-6_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,28]],"date-time":"2020-12-28T18:05:04Z","timestamp":1609178704000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-03427-6_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783030034269","9783030034276"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-03427-6_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"30 October 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ISoLA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Leveraging Applications of Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Limassol","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Cyprus","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 November 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 November 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"isola2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.isola-conference.org\/isola2018\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Equinocs","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"149","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"126","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"85% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"invitation-based event","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}