Skip to Main content Skip to Navigation
Conference papers

A Formal Security Model for Verification of Automotive Embedded Applications

Abstract : Intelligent Transport Systems (ITS) arose several years ago as a promising solution to decrease road casualties [1]. ITS are based upon heterogeneous wireless networks of vehicles and road side infrastructures. In such critical vehicular embedded systems, the safety is at stake, and so, the security of car-to-car and car-to-infrastructure communications shall be carefully taken into account, first for safety issues, but also for privacy issues. We propose a validation methodology that assists the design of such embedded systems, and based on a Formal Security Model that mainly targets model checking. If modeling of embedded in-car applications is a major issue due to system constraints and complexity, formal validation of such models shall offer a higher level of guarantee. Apart from its formal semantics, another strength of our approach relies on the decoupling between system design and security issues (e.g., attacks, requirements, and so on) whilst all are integrated in the same framework.
Complete list of metadata
Contributor : Renaud Pacalet Connect in order to contact the contributor
Submitted on : Wednesday, February 16, 2022 - 10:03:57 AM
Last modification on : Saturday, February 26, 2022 - 3:31:57 AM
Long-term archiving on: : Tuesday, May 17, 2022 - 6:15:05 PM


Files produced by the author(s)


  • HAL Id : hal-03576507, version 1


Renaud Pacalet, Gabriel Pedroza, Ludovic Apvrille. A Formal Security Model for Verification of Automotive Embedded Applications. SAFA Annual Workshop on Formal Techniques (SAFA’2010), Oct 2010, Sophia-Antipolis, France. ⟨hal-03576507⟩



Record views


Files downloads