Direction de recherche : Fabrice KORDON

Co-encadrement : POITRENAUD Denis

Contributions à l'approche automate pour la vérification de propriétés de systèmes concurrents

L'approche automate pour le model checking de propriétés temporelles à temps linéaire est une technique classique de vérification formelle de systèmes concurrents. Un système, ainsi qu'une propriété qu'on souhaite y vérifier, sont modélisés sous forme d'automates reconnaissant des mots infinis (des ?-automates). Des manipulations de ces automates permettent d'établir si le système vérifie la propriété ou non. Dans cette thèse nous nous focalisons sur un type particulier d'?-automates : les automates de Büchi généralisés basés sur les transitions (TGBA). Dans un premier temps nous revisitons les deux principales étapes de l'approche : la traduction de formules de logique temporelle à temps linéaire en TGBA et le test de vacuité (emptiness check) d'un TGBA. Pour chacune, nous proposons des améliorations des algorithmes existants, et comparons ces algorithmes pour montrer l'intérêt des TGBA. Dans un deuxième temps, nous proposons deux variations du test de vacuité. L'une peut être utilisée avec certains algorithmes qui réduisent l'automate représentant le système en regroupant ses états de façon symbolique. Elle utilise des tests d'inclusion entre ces regroupements d'états pour guider la construction à la volée de l'automate. L'autre est une généralisation aux automates de Streett (à nouveau basés sur les transitions); elle permet de prendre en compte des hypothèses d'équité forte lors de la vérification.

Deux docteurs (2014) à Sorbonne Université

Publications 2004-2017

• 2017
  • A. Duret‑Lutz : “Contributions to LTL and ?-automata for Model Checking”, habilitation à diriger des recherches, soutenance 10/02/2017 (2017)
  • E. Renault, A. Duret‑Lutz, F. Kordon, D. Poitrenaud : “Variations on Parallel Explicit Emptiness Checks for Generalized Büchi Automata”, International Journal on Software Tools for Technology Transfer, vol. 19 (6), pp. 653-673, (Springer Verlag) (2017)
• 2016
  • A. Duret‑Lutz, F. Kordon, D. Poitrenaud, E. Renault : “Heuristics for Checking Liveness Properties with Partial Order Reductions”, Automated Technology for Verification and Analysis, vol. 9938, Lecture Notes in Computer Science, Chiba, Japan, pp. 340-356, (Springer) (2016)
• 2015
  • E. Renault, A. Duret‑Lutz, F. Kordon, D. Poitrenaud : “Parallel Explicit Model Checking for Generalized Büchi Automata”, 21^th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2015, vol. 9035, Lecture Notes in Computer Science, London, United Kingdom, pp. 613-627, (Springer) (2015)
  • S. Baarir, A. Duret‑Lutz : “SAT-Based Minimization of Deterministic ω-Automata”, Logic for Programming, Artificial Intelligence, and Reasoning, Suva, Fiji, pp. 79-87 (2015)
• 2014
  • A. Ben Salem, A. Duret‑Lutz, F. Kordon, Y. Thierry‑Mieg : “Symbolic Model Checking of stutter invariant properties Using Generalized Testing Automata”, 20^th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2014, vol. 8413, Lecture Notes in Computer Science, Grenoble, France, pp. 440-454, (Springer) (2014)
  • S. Baarir, A. Duret‑Lutz : “Mechanizing the Minimization of Deterministic Generalized Büchi Automata”, Formal Techniques for Distributed Objects, Components, and Systems, vol. 8461, Lecture Notes in Computer Science, Berlin, Germany, pp. 266-283, (Springer) (2014)
• 2013
  • E. Renault, A. Duret‑Lutz, F. Kordon, D. Poitrenaud : “Three SCC-based Emptiness Checks for Generalized Büchi Automata”, Proceedings of the 19^th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'13), vol. 8312, Lecture Notes in Computer Science, Stellenbosch, South Africa, pp. 668-682, (Springer) (2013)
  • E. Renault, A. Duret‑Lutz, F. Kordon, D. Poitrenaud : “Strength-Based Decomposition of the Property Büchi Automaton for Faster Model Checking”, Proceedings of the 19^th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'13), vol. 7795, Lecture Notes in Computer Science, Rome, Italy, pp. 580-593, (Springer) (2013)
• 2012
  • A. Ben Salem, A. Duret‑Lutz, F. Kordon : “Model Checking using Generalized Testing Automata”, LNCS Transactions on Petri Nets and Other Models of Concurrency, vol. 7400 (VI), pp. 94-122, (Springer) (2012)
• 2011
  • A. Duret‑Lutz, K. Klai, D. Poitrenaud, Y. Thierry‑Mieg : “Self-Loop Aggregation Product - A New Hybrid Approach to On-the-Fly LTL Model Checking”, 9^th International Symposium on Automated Technology for Verification and Analysis (ATVA'11), vol. 6996, Lecture Notes in Computer Science, Taipei, Taiwan, Province of China, pp. 336-350, (Springer) (2011)
  • A. Ben Salem, A. Duret‑Lutz, F. Kordon : “{Generalized Büchi Automata versus Testing Automata for Model Checking}”, 2^nd workshop on Scalable and Usable Model Checking for Petri Nets and other models of Concurrency (SUMo 2011), vol. 726, CEUR-WS, Newcastle, United Kingdom, pp. 65-79, (CEUR) (2011)
• 2009
  • A. Duret‑Lutz, D. Poitrenaud, J.‑M. Couvreur : “On-the-fly Emptiness Check of Transition-Based Streett Automata”, 7^th International Symposium on Automated Technology for Verification and Analysis, ATVA 2009, vol. 5799, Lecture Notes in Computer Science, Macao, China, pp. 213-227, (Springer) (2009)
• 2007
  • A. Duret‑Lutz : “Contributions à l’approche automate pour la vérification de propriétés de systèmes concurrents”, soutenance de thèse, soutenance 10/07/2007, direction de recherche Kordon, Fabrice, co-encadrement : Poitrenaud, Denis (2007)
  • S. Baarir, A. Duret‑Lutz : “Test de vacuité pour automates de Büchi ensemblistes avec tests d’inclusion”, 6^e Colloque Francophone sur la Modélisation des Systèmes Réactifs (MSR'07), Lyon, France, pp. 19-34, (Hermes-Lavoisier) (2007)
  • S. Baarir, A. Duret‑Lutz : “Emptiness Check of Powerset Buchi Automata”, 7^th International Conference on Application of Concurrency to System Design (ACSD'07), Bratislava, Slovakia, pp. 41-50, (IEEE) (2007)
• 2006
  • S. Baarir, A. Duret‑Lutz : “Emptiness Check of Powerset Büchi Automata using Inclusion Tests”, (2006)
• 2005
  • J.‑M. Couvreur, A. Duret‑Lutz, D. Poitrenaud : “On-the-Fly Emptiness Checks for Generalized Büchi Automata”, 12^th International SPIN Workshop on Model Checking of Software, vol. 3639, Lecture Notes in Computer Science, San Francisco, United States, pp. 169-184, (Springer-Verlag) (2005)
• 2004
  • S. Baarir, J.‑M. Ilié, A. Duret‑Lutz : “Improving Reachability Analysis for Partially Symmetric High Level Petri Nets”, 12^th IEEE/ACM International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems (MASCOTS '04), Volendam, Netherlands, pp. 5-8 (2004)
  • A. Duret‑Lutz, D. Poitrenaud : “SPOT: an Extensible Model Checking Library using Transition-based Generalized Büchi Automata”, 12^th IEEE/ACM International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems (MASCOTS '04), Volendam, Netherlands, pp. 76-83, (IEEE Computer Society Press) (2004)
  • Y. Thierry‑Mieg, S. Baarir, A. Duret‑Lutz, F. Kordon : “Nouvelles techniques de Model Checking pour la vérification de systèmes complexes”, Génie logiciel : le magazine de l'ingénierie du logiciel et des systèmes, vol. 69, pp. 17-23, (Génie industriel multimédia) (2004)