On Modeling and Testing Security Properties of Vehicular Networks

In this paper a new model to formally represent some units of a vehicular network system is presented. We show how this formalism, based on finite state machines augmented with variables, allows us to represent such kind of system. We focus in a scenario of vehicle to infrastructure (V2I) communication with the Dynamic Route Planning (DRP) service as a case study. We enrich this model by a new negotiation scenario. Next, we present the notion of a test in our framework, and discuss some testing scenarios which compile some security and interoperability properties. To support the theoretical framework we translate the system specification on an IF code which we will use to generate test cases using the TestGen-IF tool. These test cases allow us to perform experiments to verify the security and interoperability properties.