Publications/renault.18.vecos

Authors

Etienne Renault

Where

Proceedings of the 12th International Conference on Verification and Evaluation of Computer and Communication Systems (VECOS'18)

Place

Grenoble, France

Type

inproceedings

Publisher

Springer, Cham

Projects

Spot

Date

2018-06-14

Abstract

The verification of temporal properties against a given system may require the exploration of its full state space. In explicit model-checking this exploration uses a Depth-First-Search (DFS) and can be achieved with multiple randomized threads to increase performance. Nonetheless the topology of the state-space and the exploration order can cap the speedup up to a certain number of threads. This paper proposes a new technique that aims to tackle this limitation by generating artificial initial states, using genetic algorithms. Threads are then launched from these states and thus explore different parts of the state space. Our prototype implementation runs 10% faster than state-of-the-art algorithms. These results demonstrate that this novel approach worth to be considered as a way to overcome existing limitations.

Documents

• Paper

Bibtex (lrde.bib)

@InProceedings{	  renault.18.vecos,
  author	= {Etienne Renault},
  title		= {Improving Parallel State-Space Exploration Using Genetic
		  Algorithms},
  booktitle	= {Proceedings of the 12th International Conference on
		  Verification and Evaluation of Computer and Communication
		  Systems (VECOS'18)},
  editor	= {Mohamed Faouzi Atig and Saddek Bensalem and Simon Bliudze
		  and Bruno Monsuez},
  address	= {Grenoble, France},
  year		= 2018,
  month		= sept,
  pages		= {133--149},
  publisher	= {Springer, Cham},
  series	= {Lecture Notes in Computer Science},
  volume	= {11181},
  abstract	= { The verification of temporal properties against a given
		  system may require the exploration of its full state space.
		  In explicit model-checking this exploration uses a
		  Depth-First-Search (DFS) and can be achieved with multiple
		  randomized threads to increase performance. Nonetheless the
		  topology of the state-space and the exploration order can
		  cap the speedup up to a certain number of threads. This
		  paper proposes a new technique that aims to tackle this
		  limitation by generating artificial initial states, using
		  genetic algorithms. Threads are then launched from these
		  states and thus explore different parts of the state space.
		  Our prototype implementation runs 10\% faster than
		  state-of-the-art algorithms. These results demonstrate that
		  this novel approach worth to be considered as a way to
		  overcome existing limitations.}
}