{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T19:43:44Z","timestamp":1694634224511},"reference-count":35,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2008,12,1]],"date-time":"2008-12-01T00:00:00Z","timestamp":1228089600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2008,12]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Formal verification of software systems is a challenge that is particularly important in the area of safety-critical automotive systems. Here, approaches like direct code verification are far too complicated, unless the verification is restricted to small textbook examples. Furthermore, the verification of application logic is of limited use in industrial context, unless the underlying operating system and the hardware are verified, too. This paper introduces a generic model stack, allowing the verification of all system layers as well as the concrete application models being used in the upper layers. The presented models and proofs close the gap between the correctness proof for the lower layers of car electronics developed at the Saarland University and the verification procedure for distributed applications developed at the Technische Universit\u00e4t M\u00fcnchen.<\/jats:p>","DOI":"10.1007\/s00165-008-0097-0","type":"journal-article","created":{"date-parts":[[2008,11,26]],"date-time":"2008-11-26T14:13:31Z","timestamp":1227708811000},"page":"637-662","source":"Crossref","is-referenced-by-count":14,"title":["On the correctness of upper layers of automotive systems"],"prefix":"10.1145","volume":"20","author":[{"given":"Jewgenij","family":"Botaschanjan","sequence":"first","affiliation":[{"name":"Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, Boltzmannstr. 3, 85748, Garching bei M\u00fcnchen, Germany"}]},{"given":"Manfred","family":"Broy","sequence":"additional","affiliation":[{"name":"Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, Boltzmannstr. 3, 85748, Garching bei M\u00fcnchen, Germany"}]},{"given":"Alexander","family":"Gruler","sequence":"additional","affiliation":[{"name":"Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, Boltzmannstr. 3, 85748, Garching bei M\u00fcnchen, Germany"}]},{"given":"Alexander","family":"Harhurin","sequence":"additional","affiliation":[{"name":"Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, Boltzmannstr. 3, 85748, Garching bei M\u00fcnchen, Germany"}]},{"given":"Steffen","family":"Knapp","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Saarland University, 66123, Saarbr\u00fccken, Germany"}]},{"given":"Leonid","family":"Kof","sequence":"additional","affiliation":[{"name":"Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, Boltzmannstr. 3, 85748, Garching bei M\u00fcnchen, Germany"}]},{"given":"Wolfgang","family":"Paul","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Saarland University, 66123, Saarbr\u00fccken, Germany"}]},{"given":"Maria","family":"Spichkova","sequence":"additional","affiliation":[{"name":"Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, Boltzmannstr. 3, 85748, Garching bei M\u00fcnchen, Germany"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","unstructured":"AbsInt Angewandte Informatik. Worst-case execution time analyzers. http:\/\/www.absint.com\/ 15.12.2006"},{"key":"e_1_2_1_2_2_2","unstructured":"AutoFocus Project. http:\/\/autofocus.in.tum.de accessed 15.12.2006"},{"key":"e_1_2_1_2_3_2","unstructured":"Beyer S B\u00f6hm P Gerke M Hillebrand M In der Rieden T Knapp S Leinenbach D Paul WJ (2005) Towards the formal verification of lower system layers in automotive systems. In: 23rd IEEE international conference on computer design: VLSI in computers and processors (ICCD\u201905). IEEE New York"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Botaschanjan J Gruler A Harhurin A Kof L Spichkova M Trachtenherz D (2006) Towards modularized verification of distributed time-triggered systems. In: Formal methods 2006. LNCS vol 4085. Springer Heidelberg August 23\u201325 2006","DOI":"10.1007\/11813040_12"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Botaschanjan J Kof L K\u00fchnel Ch Spichkova M (2005) Towards verified automotive software. In: ICSE SEAS Workshop St. Louis Missouri USA May 21 2005","DOI":"10.1145\/1083190.1083199"},{"key":"e_1_2_1_2_6_2","volume-title":"Model checking","author":"Clarke EM","year":"1999"},{"key":"e_1_2_1_2_7_2","unstructured":"FlexRay Consortium. FlexRay overview. http:\/\/www.flexray.com\/products\/protocol20overview.pdf accessed 15.12.2006"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Dalinger I Hillebrand M Paul W (2005) On the verification of memory management mechanisms. In: Borrione D Paul W (eds) CHARME 2005. LNCS. Springer Heidelberg (to appear)","DOI":"10.1007\/11560548_23"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"In der Rieden T Knapp S (2005) An approach to the pervasive formal specification and verification of an automotive system (Status Report). In: Tenth international workshop on formal methods for industrial critical systems (FMICS 05)","DOI":"10.1145\/1081180.1081195"},{"key":"e_1_2_1_2_10_2","unstructured":"European Commission (DG Enterprise and DG Information Society). eSafety forum: Summary report 2003. Technical report eSafety March 2003"},{"key":"e_1_2_1_2_11_2","unstructured":"FlexRay Consortium. http:\/\/www.flexray.com accessed 15.12.2006"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Gargano M Hillebrand M Leinenbach D Paul W (2005) On the correctness of operating system kernels. In: Hurd J Melham T (eds) TPHOLs 2005. LNCS. Springer Heidelberg","DOI":"10.1007\/11541868_1"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Huber F Sch\u00e4tz B Einert G (1997) Consistent graphical specification of distributed systems. In: Industrial applications and strengthened foundations of formal methods (FME\u201997). LNCS vol 1313. Springer Heidelberg pp 122\u2013141","DOI":"10.1007\/3-540-63533-5_7"},{"key":"e_1_2_1_2_14_2","unstructured":"IBM Rational Rose Technical Developer. http:\/\/www-306.ibm.com\/software\/awdtools\/developer\/technical\/ accessed 18.05.2006"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"In der Rieden T Leinenbach D Paul WJ (2005) Towards the pervasive verification of automotive systems. In: Correct hardware design and verification methods. Lecture Notes in Computer Science vol 3725. Springer Heidelberg pp 3\u20134","DOI":"10.1007\/11560548_3"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.1109\/2.248873"},{"key":"e_1_2_1_2_17_2","unstructured":"Knapp S (2005) Towards the verification of functional and timely behavior of an ecall implementation. Master\u2019s thesis Universit\u00e4t des Saarlandes"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Knapp S Paul W (2006) Realistic worst case execution time analysis in the context of pervasive system verification. In: Program analysis and compilation theory and practice: essays dedicated to Reinhard Wilhelm vol 4444 pp 53\u201381","DOI":"10.1007\/978-3-540-71322-7_3"},{"key":"e_1_2_1_2_19_2","unstructured":"K\u00fchnel Ch Spichkova M (2006) Upcoming automotive standards for fault-tolerant communication: FlexRay and OSEKtime FTCom. In: International workshop on engineering of fault tolerant systems (EFTS 2006) Luxembourg June 12\u201313"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"K\u00fchnel Ch Spichkova M (2007) Fault-tolerant communication for distributed embedded systems. In: Software engineering and fault tolerance. Series on Software Engineering and Knowledge Engineering vol 19. World Scientific Publishing Singapore","DOI":"10.1142\/9789812778864_0007"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Leinenbach D Paul W Petrova E (2005) Towards the formal verification of a C0 compiler. In: 3rd international conference on software engineering and formal method (SEFM 2005) Koblenz Germany","DOI":"10.1109\/SEFM.2005.51"},{"key":"e_1_2_1_2_22_2","unstructured":"The MathWorks. http:\/\/www.mathworks.com accessed 18.05.2006"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Strother Moore J (2003) A grand challenge proposal for formal methods: a verified stack. Lecture Notes in Computer Science vol 2757\/2003. Springer Berlin","DOI":"10.1007\/978-3-540-40007-3_11"},{"key":"e_1_2_1_2_24_2","unstructured":"Motor Industry Software Reliability Association (MISRA). Guidelines for the use of the C language in critical systems UK 18.05.2006"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Nipkow T Paulson LC Wenzel M (2002) Isabelle\/HOL\u2014a proof assistant for higher-order logic. LNCS vol 2283. Springer Heidelberg","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_2_1_2_26_2","unstructured":"OSEK\/VDX. Fault-Tolerant Communication\u2014Specification 1.0 2001. http:\/\/portal.osek-vdx.org\/files\/pdf\/specs\/ftcom10.pdf accessed 15.12.2006"},{"key":"e_1_2_1_2_27_2","unstructured":"OSEK\/VDX. Time-Triggered Operating System\u2014Specification 1.0 2001. http:\/\/portal.osek-vdx.org\/files\/pdf\/specs\/ttos10.pdf accessed 15.12.2006"},{"key":"e_1_2_1_2_28_2","unstructured":"OSEK\/VDX. http:\/\/www.osek-vdx.org accessed 15.12.2006"},{"key":"e_1_2_1_2_29_2","unstructured":"Paul W (2005) Lecture notes: computer architecture 2\u2014automotive systems. http:\/\/www-wjp.cs.uni-sb.de\/lehre\/vorlesung\/rechnerarchitektur2\/ws0506\/temp\/060302_CA2_AUTO.pdf December 2005"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Pnueli A Siegel M Singerman E (1998) Translation validation. In: TACAS \u201998: proceedings of the 4th international conference on tools and algorithms for construction and analysis of systems London UK 1998.Springer Heidelberg","DOI":"10.1007\/BFb0054170"},{"key":"e_1_2_1_2_31_2","unstructured":"Rushby J (1997) Systematic formal verification for fault-tolerant time-triggered algorithms. In: Dependable computing for critical applications\u20146 vol 11. IEEE Computer Society New York pp 203\u2013222"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"Schirmer N (2005) A verification environment for sequential imperative programs in Isabelle\/HOL. In: Baader F Voronkov A (eds) Logic for programming artificial intelligence and reasoning. LNAI vol 3452. Springer Heidelberg","DOI":"10.1007\/978-3-540-32275-7_26"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2002.805820"},{"key":"e_1_2_1_2_34_2","unstructured":"Verisoft Project. http:\/\/www.verisoft.de accessed 15.12.2006"},{"key":"e_1_2_1_2_35_2","first-page":"229","article-title":"Specification based test sequence generation with propositional logic","volume":"10","author":"Wimmel G","year":"2000","journal-title":"J STVR Special Issue on Specification Based Testing"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-008-0097-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-008-0097-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-008-0097-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:44:33Z","timestamp":1641483873000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-008-0097-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,12]]},"references-count":35,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2008,12]]}},"alternative-id":["10.1007\/s00165-008-0097-0"],"URL":"https:\/\/doi.org\/10.1007\/s00165-008-0097-0","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,12]]}}}