Ala Eddine Ben Salem

Combining explicit and symbolic LTL model checking using generalized testing automata

By Ala Eddine Ben Salem, Mohamed Graiet

2015-05-19

In Proceedings of the 15th international conference on application of concurrency to system design (ACSD’15)

Abstract In automata-theoretic model checking, there are mainly two approaches: explicit and symbolic. In the explicit approach, the state-space is constructed explicitly and lazily during exploration (i.e., on-the-fly). The symbolic approach tries to overcome the state-space explosion obstacle by symbolically encoding the state-space in a concise way using decision diagrams. However, this symbolic construction is not performed on-the-fly as in the explicit approach. In order to take advantage of the best of both worlds, hybrid approaches are proposed as combinations of explicit and symbolic approaches.

Continue reading

Extending testing automata to all LTL

By Ala Eddine Ben Salem

2015-05-19

In Proceedings of the 35th IFIP international conference on formal techniques for distributed objects, components and systems (FORTE’15)

Abstract An alternative to the traditional Büchi Automata (BA), called Testing Automata (TA) was proposed by Hansen et al. to improve the automata theoretic approach to LTL model checking. In previous work, we proposed an improvement of this alternative approach called TGTA (Generalized Testing Automata). TGTA mixes features from both TA and TGBA (Generalized Büchi Automata), without the disadvantage of TA, which is the second pass of the emptiness check algorithm.

Continue reading

Single-pass testing automata for LTL model checking

By Ala Eddine Ben Salem

2015-03-01

In Proceedings of the 9th international conference on language and automata theory and applications (LATA’15)

Abstract Testing Automaton (TA) is a new kind of $\omega$-automaton introduced by Hansen et al. as an alternative to the standard Büchi Automata (BA) for the verification of stutter-invariant LTL properties. Geldenhuys and Hansen shown later how to use TA in the automata-theoretic approach to LTL model checking. They propose a TA-based approach using a verification algorithm that requires two searches (two passes) and compare its performance against the BA approach.

Continue reading

Improving the model checking of stutter-invariant LTL properties

By Ala Eddine Ben Salem

2014-09-25

In

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.

Continue reading

Symbolic model checking of stutter invariant properties using generalized testing automata

By Ala Eddine Ben Salem, Alexandre Duret-Lutz, Fabrice Kordon, Yann Thierry-Mieg

2014-04-01

In Proceedings of the 20th international conference on tools and algorithms for the construction and analysis of systems (TACAS’14)

Abstract In a previous work, we showed that a kind of $\omega$-automata known as Transition-based Generalized Testing Automata (TGTA) can outperform the Büchi automata traditionally used for explicit model checking when verifying stutter-invariant properties. In this work, we investigate the use of these generalized testing automata to improve symbolic model checking of stutter-invariant LTL properties. We propose an efficient symbolic encoding of stuttering transitions in the product between a model and a TGTA.

Continue reading

Model checking using generalized testing automata

By Ala Eddine Ben Salem, Alexandre Duret-Lutz, Fabrice Kordon

2012-03-01

In Transactions on Petri Nets and Other Models of Concurrency (ToPNoC VI)

Abstract Geldenhuys and Hansen showed that a kind of $\omega$-automata known as Testing Automata (TA) can, in the case of stuttering-insensitive properties, outperform the Buchi automata traditionally used in the automata-theoretic approach to model checking (geldenhuys.06.spin?). In previous work (bensalem.sumo.2011?), we compared TA against Transition-based Generalized Buchi Automata (TGBA), and concluded that TA were more interesting when counterexamples were expected, otherwise TGBA were more efficient. In this work we introduce a new kind of automata, dubbed Transition-based Generalized Testing Automata (TGTA), that combine ideas from TA and TGBA.

Continue reading

Generalized Büchi automata versus testing automata for model checking

By Ala Eddine Ben Salem, Alexandre Duret-Lutz, Fabrice Kordon

2011-05-25

In Proceedings of the second international workshop on scalable and usable model checking for petri net and other models of concurrency (SUMO’11)

Abstract Geldenhuys and Hansen have shown that a kind of $\omega$-automaton known as testing automata can outperform the Buchi automata traditionally used in the automata-theoretic approach to model checking (geldenhuys.06.spin?). This work completes their experiments by including a comparison with generalized Buchi automata; by using larger state spaces derived from Petri nets; and by distinguishing violated formulæ (for which testing automata fare better) from verified formulæ (where testing automata are hindered by their two-pass emptiness check).

Continue reading

Search

Tags