Contribution aux tests de vacuité pour le model checking explicite

From LRDE

Revision as of 12:45, 3 April 2015 by Bot (talk | contribs)

Abstract

The automata-theoretic approach to linear time model-checking is a standard technique for formal verification of concurrent systems. The system and the property to check are modeled with omega-automata that recognizes infinite words. Operations overs these automata (synchronized product and emptiness checks) allows to determine whether the system satisfies the property or not. In this thesis we focus on a particular type of omega-automata that enable a concise representation of weak fairness properties: transitions-based generalized Büchi automata (TGBA). First we outline existing verification algorithms, and we propose new efficient algorithms for strong automata. In a second step, the analysis of the strongly connected components of the property automaton led us to develop a decomposition of this automata. This decomposition focuses on multi-strength property automata and allows a natural parallelization for already existing model-checkers. Finally, we proposed, for the first timenew parallel emptiness checks for generalized Büchi automata. Moreover, all these emptiness checks are lock-free, unlike those of the state-of-the-art. All these techniques have been implemented and then evaluated on a large benchmark.

Documents

Bibtex (lrde.bib)

@PhDThesis{	  renault.14.phd,
  author	= {Etienne Renault},
  title		= {{Contribution aux tests de vacuit\'e pour le model
		  checking explicite}},
  school	= {{Universit{\'e} Pierre et Marie Curie - Paris VI}},
  year		= 2014,
  address	= {Paris, France},
  month		= dec,
  abstract	= {The automata-theoretic approach to linear time
		  model-checking is a standard technique for formal
		  verification of concurrent systems. The system and the
		  property to check are modeled with omega-automata that
		  recognizes infinite words. Operations overs these automata
		  (synchronized product and emptiness checks) allows to
		  determine whether the system satisfies the property or not.
		  In this thesis we focus on a particular type of
		  omega-automata that enable a concise representation of weak
		  fairness properties: transitions-based generalized B\"uchi
		  automata (TGBA). First we outline existing verification
		  algorithms, and we propose new efficient algorithms for
		  strong automata. In a second step, the analysis of the
		  strongly connected components of the property automaton led
		  us to develop a decomposition of this automata. This
		  decomposition focuses on multi-strength property automata
		  and allows a natural parallelization for already existing
		  model-checkers. Finally, we proposed, for the first time,
		  new parallel emptiness checks for generalized B\"uchi
		  automata. Moreover, all these emptiness checks are
		  lock-free, unlike those of the state-of-the-art. All these
		  techniques have been implemented and then evaluated on a
		  large benchmark.}
}