Los vehículos modernos ya no son simplemente sistemas mecánicos, sino que son monitoreados y controlados por diversos sistemas electrónicos. Los sistemas críticos de seguridad de los vehículos conectados se vuelven vulnerables a ciberataques debido a la creciente interconexión. En la actualidad, el análisis de riesgos de seguridad de los vehículos conectados se basa principalmente en métodos cualitativos, mientras que estos métodos suelen ser subjetivos y carecen de consideración por la seguridad funcional. Para resolver este problema, proponemos en este documento un marco de análisis de riesgos de seguridad para vehículos conectados basado en métodos formales. En primer lugar, presentamos la arquitectura electrónica y eléctrica del vehículo conectado y analizamos las superficies de ataque de los sistemas críticos de seguridad del vehículo desde tres niveles de sensores, redes internas del vehículo y controladores. En segundo lugar, proponemos un método para modelar el objetivo de evaluación (es decir, el sistema crítico de seguridad del vehículo) como un proceso de decisión de Markov y utilizamos lógica de árbol de cómputo probabilístico para describir formalmente sus propiedades de seguridad. Luego, se utiliza un verificador de modelos probabilísticos PRISM para analizar cuantitativamente el riesgo de seguridad de los sistemas objetivo según las propiedades de seguridad. Finalmente, aplicamos el enfoque propuesto para analizar y comparar los riesgos de seguridad del sistema de advertencia de colisión bajo una arquitectura eléctrica y electrónica distribuida y centralizada. Además, desde un punto de vista práctico, proponemos un método de generación de modelos de Markov basado en un diagrama de actividades SysML, que puede simplificar nuestro proceso de modelado. Los resultados de la evaluación muestran que podemos tener una comprensión cuantitativa de los riesgos de seguridad a nivel del sistema en la etapa temprana del diseño del sistema.