Improving the Model Checking of Stutter-Invariant LTL Properties

Authors

Ala Eddine Ben Salem

Place

Paris, France

Type

phdthesis

Projects

Spot

Date

2014-09-25

Abstract

Software systems have become ubiquitous in our everyday life. They replace humans for critical tasks that involve high costs and even human lives. The serious consequences caused by the failure of such systems make crucial the use of rigorous methods for system validation. One of the widely-used formal verification methods is the automata-theoretic approach to model checking. It takes as input a model of the system and a property, and answers if the model satisfies or not the property. To achieve this goal, it translates the negation of the property in an automaton and checks whether the product of the model and this automaton is empty. Although it is automatic, this approach suffers from the combinatorial explosion of the resulting product. To tackle this problem, especially when checking stutter-invariant LTL properties, we firstly improve the two-pass verification algorithm of Testing automata (TA), then we propose a transformation of TA into a normal form (STA) that only requires a single-pass verification algorithm. We also propose a new type of automata: the TGTA. These automata also enable a check in a single-pass and without adding artificial states : it combines the benefits of TA and generalized Büchi automata (TGBA). TGTA improve the explicit and symbolic model checking approaches. In particular, by combining TGTA with the saturation technique, the performances of the symbolic approach has been improved by an order of magnitude compared to TGBA. Used in hybrid approaches TGTA prove complementary to TGBA. All the contributions of this work have been implemented in SPOT and LTS-ITSrespectively, an explicit and a symbolic open source model-checking libraries.

Documents

• Paper

Bibtex (lrde.bib)

@PhDThesis{	  bensalem.14.phd,
  author	= {Ala Eddine Ben{ S}alem},
  title		= {Improving the Model Checking of Stutter-Invariant {LTL}
		  Properties},
  school	= {{Universit{\'e} Pierre et Marie Curie - Paris VI}},
  year		= 2014,
  address	= {Paris, France},
  month		= sep,
  abstract	= {Software systems have become ubiquitous in our everyday
		  life. They replace humans for critical tasks that involve
		  high costs and even human lives. The serious consequences
		  caused by the failure of such systems make crucial the use
		  of rigorous methods for system validation. One of the
		  widely-used formal verification methods is the
		  automata-theoretic approach to model checking. It takes as
		  input a model of the system and a property, and answers if
		  the model satisfies or not the property. To achieve this
		  goal, it translates the negation of the property in an
		  automaton and checks whether the product of the model and
		  this automaton is empty. Although it is automatic, this
		  approach suffers from the combinatorial explosion of the
		  resulting product. To tackle this problem, especially when
		  checking stutter-invariant LTL properties, we firstly
		  improve the two-pass verification algorithm of Testing
		  automata (TA), then we propose a transformation of TA into
		  a normal form (STA) that only requires a single-pass
		  verification algorithm. We also propose a new type of
		  automata: the TGTA. These automata also enable a check in a
		  single-pass and without adding artificial states : it
		  combines the benefits of TA and generalized B\"uchi
		  automata (TGBA). TGTA improve the explicit and symbolic
		  model checking approaches. In particular, by combining TGTA
		  with the saturation technique, the performances of the
		  symbolic approach has been improved by an order of
		  magnitude compared to TGBA. Used in hybrid approaches TGTA
		  prove complementary to TGBA. All the contributions of this
		  work have been implemented in SPOT and LTS-ITS,
		  respectively, an explicit and a symbolic open source
		  model-checking libraries.}
}