I was invited to give a talk to Coventry University’s Institute for Future Transport and Cities on my work performed for FAIR-SPACE which investigated a formal verification of security properties of the generation of Cooperative Awareness Messages. One of the conclusions of this presentation was the difficulty of verifying non-functional security properties.
The presentation is available here