{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:41:44Z","timestamp":1750308104551,"version":"3.41.0"},"reference-count":16,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2005,5,21]],"date-time":"2005-05-21T00:00:00Z","timestamp":1116633600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGSOFT Softw. Eng. Notes"],"published-print":{"date-parts":[[2005,7]]},"abstract":"<jats:p>\n            Automotive software is one of the most challenging fields of software engineering: it must meet real time requirements, is safety critical and distributed over multiple processors. With the increasing complexity of automotive software, as for example in the case of drive-by-wire, automated driving and driver assitents, software correctness becomes more and more a crucial issue. In order that these innovations can become reality, it is necessary to be able to\n            <jats:italic>guarantee<\/jats:italic>\n            software correctness.The presented work aims at verification of automotive software. For this purpose it introduces a verification approach, including a framework of verified modules which assists the verification of the actual application. Feasibility of this approach was validated on a case study that also showed how verification can be integrated into the development process.\n          <\/jats:p>","DOI":"10.1145\/1082983.1083199","type":"journal-article","created":{"date-parts":[[2005,11,7]],"date-time":"2005-11-07T19:28:32Z","timestamp":1131391712000},"page":"1-6","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Towards verified automotive software"],"prefix":"10.1145","volume":"30","author":[{"given":"J.","family":"Botaschanjan","sequence":"first","affiliation":[{"name":"Institut f\u00fcr Informatik, Garching, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"L.","family":"Kof","sequence":"additional","affiliation":[{"name":"Institut f\u00fcr Informatik, Garching, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"C.","family":"K\u00fchnel","sequence":"additional","affiliation":[{"name":"Institut f\u00fcr Informatik, Garching, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M.","family":"Spichkova","sequence":"additional","affiliation":[{"name":"Institut f\u00fcr Informatik, Garching, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2005,5,21]]},"reference":[{"volume-title":"FlexRay Communication System - Protocol Specification - Version 2.0","year":"2004","author":"FlexRay Consortium","key":"e_1_2_1_1_1"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/780732.780754"},{"volume-title":"eSafety forum: Summary report","year":"2003","author":"European Commission (DG Enterprise and DG Information Society).","key":"e_1_2_1_3_1"},{"key":"e_1_2_1_4_1","unstructured":"FlexRay Consortium. http:\/\/www.flexray.com.  FlexRay Consortium. http:\/\/www.flexray.com."},{"volume-title":"FlexRay Communication System - Bus Guardian Specification - Version 2.0","year":"2004","author":"FlexRay Consortium","key":"e_1_2_1_5_1"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/647538.729851"},{"key":"e_1_2_1_8_1","unstructured":"L4 microkernel. http:\/\/os.inf.tu-dresden. de\/L4\/.  L4 microkernel. http:\/\/os.inf.tu-dresden. de\/L4\/."},{"key":"e_1_2_1_9_1","series-title":"LNCS","volume-title":"Isabelle\/HOL --- A Proof Assistant for Higher-Order Logic","author":"Nipkow T.","year":"2002"},{"key":"e_1_2_1_10_1","unstructured":"OSEK\/VDX. http:\/\/www.osek-vdx.org.  OSEK\/VDX. http:\/\/www.osek-vdx.org."},{"volume-title":"Fault-Tolerant Communication - Specification 1.0","year":"2001","author":"VDX.","key":"e_1_2_1_11_1"},{"volume-title":"Time-Triggered Operating System - Specification 1.0","year":"2001","author":"VDX.","key":"e_1_2_1_12_1"},{"key":"e_1_2_1_13_1","series-title":"LNCS","first-page":"151","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Pnueli A."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/646847.707100"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/645790.667833"},{"volume-title":"Documentation and modelling of the ipc mechanism in the 14 kernel. Master's thesis","year":"2003","author":"Tverdyshev S.","key":"e_1_2_1_16_1"},{"key":"e_1_2_1_17_1","unstructured":"Verisoft Project. http:\/\/www.verisoft.de\/.  Verisoft Project. http:\/\/www.verisoft.de\/."}],"container-title":["ACM SIGSOFT Software Engineering Notes"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1082983.1083199","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1082983.1083199","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T16:08:05Z","timestamp":1750262885000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1082983.1083199"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,5,21]]},"references-count":16,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2005,7]]}},"alternative-id":["10.1145\/1082983.1083199"],"URL":"https:\/\/doi.org\/10.1145\/1082983.1083199","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1083190.1083199","asserted-by":"subject"}]},"ISSN":["0163-5948"],"issn-type":[{"type":"print","value":"0163-5948"}],"subject":[],"published":{"date-parts":[[2005,5,21]]},"assertion":[{"value":"2005-05-21","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}