Showing
1 changed file
with
6 additions
and
6 deletions
1 | -#VerifCar | 1 | +# VerifCar |
2 | 2 | ||
3 | VerifCar is a framework devoted to validation of decision policies of communicating autonomous vehicles (CAVs). | 3 | VerifCar is a framework devoted to validation of decision policies of communicating autonomous vehicles (CAVs). |
4 | 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. | 4 | 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. |
5 | The framework is designed in particular to be exhaustive on the non-determinism induced by the latency, communication delays and concurrency features. | 5 | The framework is designed in particular to be exhaustive on the non-determinism induced by the latency, communication delays and concurrency features. |
6 | 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". | 6 | 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". |
7 | 7 | ||
8 | -##The UPPAAL tool | 8 | +## The UPPAAL tool |
9 | 9 | ||
10 | The model is designed for verification through the model checking tool UPPAAL. | 10 | The model is designed for verification through the model checking tool UPPAAL. |
11 | In order to use VerifCar, first download the stable version of UPPAAL at http://www.uppaal.org/ | 11 | In order to use VerifCar, first download the stable version of UPPAAL at http://www.uppaal.org/ |
12 | It is preferable for a better computation time to use a depth-first exploration when checking queries with VerifCar. | 12 | It is preferable for a better computation time to use a depth-first exploration when checking queries with VerifCar. |
13 | 13 | ||
14 | -##Templates | 14 | +## Templates |
15 | 15 | ||
16 | -###VerifCar_clean_template | 16 | +### VerifCar_clean_template |
17 | 17 | ||
18 | This template implements the model along with a time-to-collision algorithm that can be used as a part of a querry input. | 18 | This template implements the model along with a time-to-collision algorithm that can be used as a part of a querry input. |
19 | It does not implements any decision algorithm. | 19 | It does not implements any decision algorithm. |
... | @@ -22,11 +22,11 @@ Places where variables should be added to the data structure for decision or com | ... | @@ -22,11 +22,11 @@ Places where variables should be added to the data structure for decision or com |
22 | 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. | 22 | 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. |
23 | 23 | ||
24 | 24 | ||
25 | -###VerifCar_template_decision_algorithm | 25 | +### VerifCar_template_decision_algorithm |
26 | 26 | ||
27 | 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". | 27 | 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". |
28 | 28 | ||
29 | -##Source Repository | 29 | +## Source Repository |
30 | 30 | ||
31 | 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". | 31 | 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". |
32 | Each .xml file contains a model and a set of queries that can be checked with the UPPAAL tool. | 32 | Each .xml file contains a model and a set of queries that can be checked with the UPPAAL tool. | ... | ... |
-
Please register or login to post a comment