Car electronics are often distributed real-time systems comprising hardware (processor and devices), an operating system, and applications. When going for verification, in addition to functional correctness properties one has to consider safety and time-critical properties. In this talk I will present a verification approach that aims at pervasive verification of such systems. To show applicability of my model stack, I consider an automatic emergency call system, eCall, as proposed by the EU commission to become mandatory for mass production cars from 2009 on.