#VerifCar
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.