Title:	Formal Verification of Group Communication
DNr:	LiU-2017-00089-9
Project Type:	LiU Compute
Principal Investigator:	Mikael Asplund <mikael.asplund@liu.se>
Affiliation:	Linköpings universitet
Duration:	2017-03-31 – 2021-04-01
Classification:	10201
Homepage:	http://www.ida.liu.se/~mikas34/ceniit/
Keywords:

Abstract

This project focuses on how to achieve reliable coordination mechanisms between vehicles which can be formally shown to fulfil a given specification. Such mechanisms would be of great importance when designing application level components, since this will reduce the number of special cases (e.g., a communication failure during a critical phase) which would otherwise have to be dealt with by the application designers. This has the potential to significantly reduce development costs (finding faults early), and to increase the reliability of the end products. Part of the project relates to formally verifying correctness of group communication algorithms. Such verification has already been carried out using tools such as PRISM and Z3. As the scale of the problem increases, more computer resources are required. This is the reason for the application to use NSC resources.