VerifCar is a framework devoted to validation of decision policies of communicating autonomous vehicles (CAVs).
It is composed of a scalable model of a CAV system optimized for formal verification together with a method of calculating indicators allowing to evaluate the quality of a given autonomous vehicle decision policy.
The framework is designed in particular to be exhaustive on the non-determinism induced by the latency, communication delays and concurrency features.
In order to use the framework, it is strongly recommended to read the academic paper intitled "VerifCar : a framework for modeling and model-checking communicating autonomous vehicles".
##The UPPAAL tool
The model is designed for verification through the model checking tool UPPAAL.
In order to use VerifCar, first download the stable version of UPPAAL at http://www.uppaal.org/
It is preferable for a better computation time to use a depth-first exploration when checking queries with VerifCar.
##Templates
###VerifCar_clean_template
This template implements the model along with a time-to-collision algorithm that can be used as a part of a querry input.
It does not implements any decision algorithm.
Places where the decision algorithm should be implemented are notified by "//INSTRUCTION" marks followed with instructions on the process.
Places where variables should be added to the data structure for decision or communication needs are notified by "//INSTRUCTION" marks followed with instructions on the process.
The template features 3 vehicles on a given environment, exhaustives instructions are given on changes requiered to add or remove vehicles, or modify the environmental parameters.
###VerifCar_template_decision_algorithm
This template implements a decision algorithm developped for experimentation purpose and used in the academic paper intitled "VerifCar : a framework for modeling and model-checking communicating autonomous vehicles".
##Source Repository
The repository named "Source for "VerifCar : a framework for modeling and model-checking communicating autonomous vehicles"" contains the sources that can be used to reproduce any of the experimentations described in the academic paper intitled "VerifCar : a framework for modeling and model-checking communicating autonomous vehicles".
Each .xml file contains a model and a set of queries that can be checked with the UPPAAL tool.
The files are gathered in regard to the Table in which they appear in the paper.