Name Last Update
Source for "VerifCar : a framework for modeling and model-checking communicating autonomous vehicles" Loading commit data...
README.md Loading commit data...
VerifCar_template_clean.xml Loading commit data...
VerifCar_template_decision_algorithm.xml Loading commit data...

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.