{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T20:26:28Z","timestamp":1743107188081,"version":"3.40.3"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030480769"},{"type":"electronic","value":"9783030480776"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","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":[[2020]]},"DOI":"10.1007\/978-3-030-48077-6_30","type":"book-chapter","created":{"date-parts":[[2020,5,21]],"date-time":"2020-05-21T23:12:43Z","timestamp":1590102763000},"page":"382-397","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["A Verified Low-Level Implementation of the Adaptive Exterior Light and Speed Control System"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6712-9798","authenticated-orcid":false,"given":"Sebastian","family":"Krings","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7256-9560","authenticated-orcid":false,"given":"Philipp","family":"K\u00f6rner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0819-5554","authenticated-orcid":false,"given":"Jannik","family":"Dunkelau","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6751-0369","authenticated-orcid":false,"given":"Chris","family":"Rutenkolk","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,5,22]]},"reference":[{"key":"30_CR1","unstructured":"MISRA C:2012 - Guidelines for the use of the C language in critical systems. MISRA (2013)"},{"key":"30_CR2","unstructured":"General Specification of Basic Software Modules. AUTOSAR, Munich (2019)"},{"key":"30_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-27777-4_1","volume-title":"Extreme Programming and Agile Methods - XP\/Agile Universe 2004","author":"H Baumeister","year":"2004","unstructured":"Baumeister, H.: Combining formal specifications with test driven development. In: Zannier, C., Erdogmus, H., Lindstrom, L. (eds.) XP\/Agile Universe 2004. LNCS, vol. 3134, pp. 1\u201312. Springer, Heidelberg (2004). \nhttps:\/\/doi.org\/10.1007\/978-3-540-27777-4_1"},{"key":"30_CR4","series-title":"Kent Beck Signature Book","volume-title":"Test-Driven Development: By Example","author":"K Beck","year":"2003","unstructured":"Beck, K.: Test-Driven Development: By Example. Kent Beck Signature Book. Addison-Wesley, Boston (2003)"},{"key":"30_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193\u2013207. Springer, Heidelberg (1999). \nhttps:\/\/doi.org\/10.1007\/3-540-49059-0_14"},{"key":"30_CR6","doi-asserted-by":"crossref","unstructured":"Boogerd, C., Moonen, L.: Assessing the value of coding standards: an empirical study. In: Proceedings ICSM, pp. 277\u2013286. IEEE (2008)","DOI":"10.1109\/ICSM.2008.4658076"},{"issue":"4","key":"30_CR7","doi-asserted-by":"crossref","first-page":"34","DOI":"10.1109\/52.391826","volume":"12","author":"JP Bowen","year":"1995","unstructured":"Bowen, J.P., Hinchey, M.G.: Seven more myths of formal methods. IEEE Softw. 12(4), 34\u201341 (1995)","journal-title":"IEEE Softw."},{"key":"30_CR8","unstructured":"Cadar, C., Dunbar, D., Engler, D.R., et al.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proceedings OSDI, vol. 8, pp. 209\u2013224. USENIX Association (2008)"},{"key":"30_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"442","DOI":"10.1007\/978-3-319-89963-3_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Chalupa","year":"2018","unstructured":"Chalupa, M., Vitovsk\u00e1, M., Strej\u010dek, J.: SYMBIOTIC\u00a05: boosted instrumentation. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 442\u2013446. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-89963-3_29"},{"key":"30_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/978-3-319-52228-9_4","volume-title":"Unifying Theories of Programming","author":"M Chen","year":"2017","unstructured":"Chen, M., Ravn, A.P., Wang, S., Yang, M., Zhan, N.: A two-way path between formal and informal design of embedded systems. In: Bowen, J.P., Zhu, H. (eds.) UTP 2016. LNCS, vol. 10134, pp. 65\u201392. Springer, Cham (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-319-52228-9_4"},{"key":"30_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168\u2013176. Springer, Heidelberg (2004). \nhttps:\/\/doi.org\/10.1007\/978-3-540-24730-2_15"},{"key":"30_CR12","doi-asserted-by":"crossref","unstructured":"Clarke, E., Kroening, D., Yorav, K.: Behavioral consistency of C and Verilog programs using bounded model checking. In: Proceedings DAC, pp. 368\u2013371. IEEE (2003)","DOI":"10.21236\/ADA461052"},{"key":"30_CR13","doi-asserted-by":"crossref","unstructured":"Fathy, H.K., Filipi, Z.S., Hagena, J., Stein, J.L.: Review of hardware-in-the-loop simulation and its prospects in the automotive area. In: Modeling and Simulation for Military Applications, vol. 6228. SPIE (2006)","DOI":"10.1117\/12.667794"},{"issue":"5","key":"30_CR14","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1109\/52.57887","volume":"7","author":"A Hall","year":"1990","unstructured":"Hall, A.: Seven myths of formal methods. IEEE Softw. 7(5), 11\u201319 (1990)","journal-title":"IEEE Softw."},{"key":"30_CR15","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/978-3-319-07512-9_5","volume-title":"ABZ 2014: The Landing Gear Case Study","author":"D Hansen","year":"2014","unstructured":"Hansen, D., Ladenberger, L., Wiegard, H., Bendisposto, J., Leuschel, M.: Validation of the ABZ landing gear system using ProB. In: Boniol, F., Wiels, V., Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. CCIS, vol. 433, pp. 66\u201379. Springer, Cham (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-319-07512-9_5"},{"key":"30_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/978-3-319-91271-4_20","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"D Hansen","year":"2018","unstructured":"Hansen, D., et al.: Using a formal B model at runtime in a demonstration of the ETCS hybrid level 3 concept with real trains. In: Butler, M., Raschke, A., Hoang, T.S., Reichl, K. (eds.) ABZ 2018. LNCS, vol. 10817, pp. 292\u2013306. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-91271-4_20"},{"issue":"5","key":"30_CR17","doi-asserted-by":"crossref","first-page":"475","DOI":"10.1016\/j.infsof.2006.07.004","volume":"49","author":"L Hatton","year":"2007","unstructured":"Hatton, L.: Language subsetting in an industrial context: a comparison of MISRA C 1998 and MISRA C 2004. Inf. Softw. Technol. 49(5), 475\u2013482 (2007)","journal-title":"Inf. Softw. Technol."},{"key":"30_CR18","doi-asserted-by":"crossref","unstructured":"Houdek, F., Raschke, A.: Adaptive exterior light and speed control system (2020)","DOI":"10.1007\/978-3-030-48077-6_24"},{"key":"30_CR19","unstructured":"ISO: Road vehicles - functional safety (2011)"},{"issue":"7","key":"30_CR20","doi-asserted-by":"crossref","first-page":"1163","DOI":"10.1016\/j.jss.2007.08.026","volume":"81","author":"M Short","year":"2008","unstructured":"Short, M., Pont, M.J.: Assessment of high-integrity embedded automotive control systems using hardware in the loop simulation. J. Syst. Softw. 81(7), 1163\u20131183 (2008)","journal-title":"J. Syst. Softw."},{"key":"30_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/978-3-319-29628-9_6","volume-title":"Engineering Trustworthy Software Systems","author":"M Yang","year":"2016","unstructured":"Yang, M., Zhan, N.: Combining formal and informal methods in\u00a0the\u00a0design of spacecrafts. In: Liu, Z., Zhang, Z. (eds.) SETSS 2014. LNCS, vol. 9506, pp. 290\u2013323. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-29628-9_6"},{"key":"30_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"376","DOI":"10.1007\/3-540-63166-6_37","volume-title":"Computer Aided Verification","author":"J Yuan","year":"1997","unstructured":"Yuan, J., Shen, J., Abraham, J., Aziz, A.: On combining formal and informal verification. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 376\u2013387. Springer, Heidelberg (1997). \nhttps:\/\/doi.org\/10.1007\/3-540-63166-6_37"}],"container-title":["Lecture Notes in Computer Science","Rigorous State-Based Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-48077-6_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,22]],"date-time":"2020-05-22T00:04:49Z","timestamp":1590105889000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-48077-6_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030480769","9783030480776"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-48077-6_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"22 May 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ABZ","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Rigorous State-Based Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Ulm","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 May 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 May 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"abz2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/abz2020.uni-ulm.de\/","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":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"61","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":"12","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":"9","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":"20% - 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":"3","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":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6 case study contributions, 6 PhD-Symposium-contributions, 2 invited papers. The conference was cancelled due to the COVID-19 pandemic.","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)"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}