Abstract
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ät München.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
AbsInt Angewandte Informatik. Worst-case execution time analyzers. http://www.absint.com/, 15.12.2006
AutoFocus Project. http://autofocus.in.tum.de, accessed 15.12.2006
Beyer S, Böhm 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’05). IEEE, New York
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–25 2006
Botaschanjan J, Kof L, Kühnel Ch, Spichkova M (2005) Towards verified automotive software. In: ICSE, SEAS Workshop, St. Louis, Missouri, USA, May 21 2005
Clarke EM, Grumberg O, Peled DA (1999) Model checking. The MIT Press, Cambridge
FlexRay Consortium. FlexRay overview. http://www.flexray.com/products/protocol20overview.pdf, accessed 15.12.2006
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)
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)
European Commission (DG Enterprise and DG Information Society). eSafety forum: Summary report 2003. Technical report, eSafety, March 2003
FlexRay Consortium. http://www.flexray.com, accessed 15.12.2006
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
Huber F, Schätz B, Einert G (1997) Consistent graphical specification of distributed systems. In: Industrial applications and strengthened foundations of formal methods (FME’97). LNCS, vol 1313. Springer, Heidelberg, pp 122–141
IBM Rational Rose Technical Developer. http://www-306.ibm.com/software/awdtools/developer/technical/, accessed 18.05.2006
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–4
Kopetz H, Grünsteidl G (1994) TTP—a protocol for fault-tolerant real-time systems. Computer 27(1): 14–23
Knapp S (2005) Towards the verification of functional and timely behavior of an ecall implementation. Master’s thesis, Universität des Saarlandes
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–81
Kühnel 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–13
Kühnel 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
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
The MathWorks. http://www.mathworks.com, accessed 18.05.2006
Strother Moore J (2003) A grand challenge proposal for formal methods: a verified stack. Lecture Notes in Computer Science, vol 2757/2003. Springer, Berlin
Motor Industry Software Reliability Association (MISRA). Guidelines for the use of the C language in critical systems, UK, 18.05.2006
Nipkow T, Paulson LC, Wenzel M (2002) Isabelle/HOL—a proof assistant for higher-order logic. LNCS, vol 2283. Springer, Heidelberg
OSEK/VDX. Fault-Tolerant Communication—Specification 1.0, 2001. http://portal.osek-vdx.org/files/pdf/specs/ftcom10.pdf, accessed 15.12.2006
OSEK/VDX. Time-Triggered Operating System—Specification 1.0, 2001. http://portal.osek-vdx.org/files/pdf/specs/ttos10.pdf, accessed 15.12.2006
OSEK/VDX. http://www.osek-vdx.org, accessed 15.12.2006
Paul W (2005) Lecture notes: computer architecture 2—automotive systems. http://www-wjp.cs.uni-sb.de/lehre/vorlesung/rechnerarchitektur2/ws0506/temp/060302_CA2_AUTO.pdf, December 2005
Pnueli A, Siegel M, Singerman E (1998) Translation validation. In: TACAS ’98: proceedings of the 4th international conference on tools and algorithms for construction and analysis of systems, London, UK, 1998.Springer, Heidelberg
Rushby J (1997) Systematic formal verification for fault-tolerant time-triggered algorithms. In: Dependable computing for critical applications—6, vol 11. IEEE Computer Society, New York, pp 203–222
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
Sifakis J, Tripakis S, Yovine S (2003) Building models of real-time systems from application software. Proc IEEE 91(1): 100–111
Verisoft Project. http://www.verisoft.de, accessed 15.12.2006
Wimmel G, Lötzbeyer H, Pretschner A, Slotosch O (2000) Specification based test sequence generation with propositional logic. J STVR Special Issue on Specification Based Testing, 2000, 10:229–248
Author information
Authors and Affiliations
Corresponding author
Additional information
Communicated by C.B. Jones
The work of J. Botaschanjan, A. Gruler, A. Harhurin, S. Knapp, L. Kof, and M. Spichkova was partially funded by the German Federal Ministry of Education and Technology (BMBF) in Verisoft project under grant 01 IS C38.
Rights and permissions
About this article
Cite this article
Botaschanjan, J., Broy, M., Gruler, A. et al. On the correctness of upper layers of automotive systems. Form Asp Comp 20, 637–662 (2008). https://doi.org/10.1007/s00165-008-0097-0
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-008-0097-0