Whether Software Defined Vehicles (SDV) or Software Defined Radio (SDR), both models provide an abstract reference for real designs. These software defined models can be used not just for guidance during design, but also they can enable formally verifying and evidence-based logs to check the compliance of such complex systems with safety (case SDV) and/or privacy (SDR) specifications and hence can be seen as a the cornerstone for -not only trustworthy contract based design- but also for further safety regulations and GDPR compliance checks and violations capturing. 

To enable using these models for that purpose, formally specifying the properties of these interfaces inside these reference models where contracts and monitoring specifications can be defined is the first
step. This includes understanding what are the interfaces in these reference models are mapped to in reality and defining which kind of abstractions are needed to compare the data exchanged at those
interfaces in the reference models vs. what they correspond to in the real interfaces. 

Basics of formal methods

Experience with SAT/SMT solvers

Preferably C or C++ project based experience