VerTeCs Project - Irisa/INRIA Rennes

Stages Master 2 Recherche: 2009-2010

Test d'automates temporisés
Mots clés : Test, méthodes formelles, automates temporisés, déterminisation.
Model checking des structures rationnelles déterministes
Mots clés :Automates, Rationalité, Logique, Langages, Déterminisme
Autour de la déterminisation des réseaux de Petri
Mots clés :Méthodes formelles, réseaux de Petri, déterminisation.
Cadre formel pour le diagnostic de propriétés sur les systèmes à événements discrets
Mots clés : Diagnostic, Discrete Event Systems, Automates, Logique, Sûreté, Intermittence
Automates communicants temporisés
Mots clés :vérification, canaux FIFO à pertes, automates temporisés
Timed rational graphs
Mots clés :Rational graphs, Timed systems, Languages, Logic.
Assurer / préserver les propriétés de disponibilitédans des systèmes d'informations
Mots clés :Sécurité, disponibilité, Système à événements discrets, Automates, Théorie du contrôle.

Test d'automates temporisés
Mots clés : Test, méthodes formelles, automates temporisés, déterminisation.
Encadreurs: Nathalie Bertrand (Nathalie.Bertrand@irisa.fr), Thierry Jéron (Thierry.Jeron@irisa.fr),
Description : Le modèle des automates temporisés d'Alur et Dill [AD94] est un modèle standard pour représenter des systèmes réactifs soumis à des contraintes temps-réelles, et sur lequel beaucoup de recherches se sont focalisées sur la vérification formelle, le contrôle, le diagnostic et le test. Dans ce stage, on s'intéresse plus particulièrement à La génération automatique de tests de conformité à partir de tels modèles. Cette problématique a déjà été étudiée, avec l'émergence de théories du test de conformité et des algorithmes de géneration fondés sur la vérification symbolique [NS03,KT04,BB05,ST08].
Un des problèmes auxquels ces algorithmes doivent faire face est celui de la déterminisation des automates temporisés, impossible dans le cas général. Les solutions existantes consistent, soit à se restreindre à des sous-classes déterminisables [NS03], soit à déterminiser à la volée (le test est calculé pendant son exécution) [KT04,BB05], soit à se ramener à un temps discret en perdant en précision [KT04]. Récemment, [BBBB09] propose une heuristique de déterminisation et une condition suffisante pour que celle-ci termine, condition satisfaite par plusieurs sous-classes connues d'automates temporisés déterminisables. L'utilisation de cette procédure dans le contexte de la génération de tests ouvre la voix à de nouveaux algorithmes de génération de tests produisant des tests directement sous la forme d'automates temporisés.
Après une étude bibliographique basée sur les références citées ici, le premier but du stage sera d'étudier comment adapter la procédure de déterminisation à la génération de tests. En fonction des avancées, un approfondissement possible consiste à étudier les problématiques de couverture de test pour les automates temporisés, en s'attachant à exhiber des critères sémantiques plus significatifs que les critères de couverture syntaxiques usuels [ZHM97] (en s'inspirant par exemple des travaux de [ND07]), et à exhiber les algorithmes de génération de tests correspondants.
Prérequis : la réalisation de ce stage nécessite de suivre le module VTS.
Bibliographie :
- [AD94] R. Alur and D. L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183-235, 1994.
- [BBBB09] C. Baier, N. Bertrand, P. Bouyer, Th. Brihaye, When are timed automata determinizable?, in 36th International Colloquium on Automata, Languages and Programming (ICALP'09), Rhodes, Greece, LNCS No 5556, p 43-54, July 2009.
- [BB05] E. Brinksma and L. B. Briones. A test generation framework for quiescent real-time systems. In Formal Approaches to Software Testing, 4th International Workshop, FATES 2004, Linz, Austria, LNCS No 3395. Springer, 2005.
- [KT04] M. Krichen and S. Tripakis. Black-box conformance testing for real-time systems. In 11th International SPIN Workshop, Barcelona, Spain, LNCS No 2989. Springer, 2004.
- [ND07] T. Nahhal and T. Dang. Test Coverage for Continuous and Hybrid Systems. In CAV 2007 - Computer Aided Verification, Berlin, Germany, July 2007.
- [NS03] B. Nielsen and A. Skou. Automated test generation from timed automata. International Journal on Software Tools for Technology Transfer (STTT), vol 5, 2003.
- [ST08] J. Schmaltz and J. Tretmans. On conformance testing for timed systems. In 6th International Conference, FORMATS 2008, Saint Malo, France, number 5215 in LNCS, p 15-17. Springer, 2008.
- [ZHM97] Zhu, H., Hall, P. A., and May, J. H. 1997. Software unit test coverage and adequacy. ACM Computing Survey, 29, 4 (Dec. 1997), 366-427.
Model checking des structures rationnelles déterministes
Mots clés : Automates, Rationalité, Logique, Langages, Déterminisme
Encadreur: Christophe Morvan. Projet VerTeCs, tel 02-99-84-25-15, F 207
(christophe.morvan@irisa.fr)
Description : Le regular model checking [1] consiste à déterminer les propriétés de systèmes dont les états sont des mots sur un alphabet donné, et dont certains sous-ensembles rationnels d'états sont particularisés. En général, les transitions de tels systèmes sont elles-mêmes caractérisées par des automates finis étiquetés par des paires de mots.
Il existe principalement deux types d'automates sur les paires : ceux qui sont synchrones définissent les relations automatiques (ou reconnaissables) et ceux qui ne le sont pas définissent les relations rationnelles. Les graphes définis par ces objets ont été largement étudiés [1, 2, 3], ils sont expressifs, et possèdent un grand nombre de propriétés décidables. Ces propriétés reposent, pour la plupart, sur la nature des automates qui caractérisent ces relations. Il y a eu relativement peu de travaux visant à étudier de telles familles de graphes sous l'angle structurel (principalement les arbres [4] et les oméga-mots [5]).
L'objet de ce travail consiste à étudier les spécificités de ces graphes lorsqu'ils sont déterministes (ce travail a été ébauché dans [6], sous l'angle des langages reconnus). On prévoit également de considérer plusieurs notions de déterminisme suivant qu'on s'intéresse exclusivement à la structure, ou qu'on s'intéresse également à la dynamique sous-jacente à cette structure.
Bibliographie :
1. [1] M. Nilsson : Regular Model Checking, Ph.D. Thesis, 2005.
2. [2] C. Morvan : On rational graphs, Fossacs 2000. LNCS 1784 pp. 252 - 266
3. [3] A. Blumensath, E. Grädel : Automatic Structures. LICS 2000, pp. 51-62.
4. [4] A. Carayol, C. Morvan : On rational trees, CSL 2006. LNCS 4207
5. [5] V. Bárány : A Hierarchy of Automatic omega-Words having a Decidable MSO Theory. RAIRO - Theor. Inf. Appl., vol. 42, pp. 417-450, 2008.
6. [6] A. Carayol, A. Meyer : Context-Sensitive Languages, Rational Graphs and Determinism. LMCS 2(2), 2006
Autour de la déterminisation des réseaux de Petri
Mots clés : Méthodes formelles, réseaux de Petri, déterminisation.
Encadreurs: Nathalie Bertrand (Nathalie.Bertrand@irisa.fr), Claude Jard (Claude.Jard@bretagne.ens-cachan.fr)
Description :Les réseaux de Petri constituent un modèle bien adapté à la représentation des systèmes concurrents. Même s'ils ont été introduits il y a plusieurs décennies, de nombreuses questions, résolues pour d'autres modèles comme les automates finis, à pile, ou temporisés, restent ouvertes. En particulier, le problème de déterminisation lié à celui de l'élimination des transitions silencieuses n'ont été que très peu étudiés. Wimmel a montré qu'il était possible d'éliminer les transitions silencieuses pour une sous-classe de réseaux de Petri (sans conflit) tout en préservant le language des traces [Wim04].
Le tout premier objectif du stage sera de définir proprement les problèmes de déterminisation et d'élimination des transitions silencieuses pour les réseaux de Petri. Il s'agit ensuite d'étendre le résultat de Wimmel à d'autres classes de réseaux de Petri.
Deux pistes sont proposées :
- partant de la méthode de Wimmel, étudier les conséquences de la présence de conflit dans les réseaux,
- considérer des réseaux sans conflit, mais temporisés [Mer74]. Pour celà, on pourra s'inspirer de travaux récents sur les automates temporisés [BBBB09, DL09].
Prérequis : la réalisation de ce stage nécessite de suivre le module VTS.
Bibliographie :
- [BBBB09] C. Baier, N. Bertrand, P. Bouyer, Th. Brihaye. When are timed automata determinizable? ICALP'09
- [DL09] C. Dima, R. Lanotte, Removing all silent transitions form timed automata. Formats'09.
- [Mer74] P. Merlin. A Study of the Recoverability of Computing Systems. PhD thesis. 1974.
- [Wim04] H. Wimmel. Eliminating internal behaviour in Petri nets. ICAPTN'04.
Cadre formel pour le diagnostic de propriétés sur les systèmes à événements discrets
Mots clés : Diagnostic, Discrete Event Systems, Automates, Logique, Sûreté, Intermittence
Encadreurs: Thierry Jéron, Hervé Marchand, Christophe Morvan. Projet VerTeCs, tel 02-99-84 {75-02, 75-09, 25-15}, F203, F201 & F207
(thierry.jeron@irisa.fr, herve.marchand@irisa.fr, christophe.morvan@irisa.fr)
Description : Dans ce stage, on s'intéressera au diagnostic de systèmes à événements discrets. Étant donné le modèle d'un système et une propriété, le diagnostic consiste à observer certains événements du système pendant son exécution (on se place dans le contexte d'une observation partielle), et à déterminer en temps borné (et en ligne a priori) si les exécutions compatibles avec l'observation violent la propriété. Deux problèmes se posent : le système est il diagnosticable (i.e. est'il toujours possible d'inférer en temps borné que la propriété a été violée), et comment construire un diagnostiqueur relativement à la propriété. Dans le cadre de modèles de systèmes de type systèmes de transitions, et de propriétés de sûreté (une fois violées, elles le restent), le problème est résolu par des algorithmes assez standards sur les automates. Le problème est beaucoup moins abordé pour des propriétés intermittentes, où une exécution peut varier entre la violation et la satisfaction, propriétés cependant cruciales à diagnostiquer.
L'étude bibliographique du stage aura pour but de dresser un panorama compréhensible des contributions à ce problème en essayant d'en dégager les idées principales. Le stage consistera ensuite à définir un cadre formel général permettant de poser clairement les problèmes de diagnostic de propriétés quelconques (de sûreté ou intermittentes, etc), et de définir les algorithmes de vérification de diagnosabilité et de construction de diagnostiqueurs associés. Le cadre formel sera basé sur une sémantique précise des observations (quelles sont les exécutions compatibles avec une séquence d'observation), l'expression des propriétés à diagnostiquer (automates ou logique), et l'expression des problèmes de diagnostic. Les algorithmes seront si possible implémentés.
Bibliographie :

Automates communicants temporisés
Mots clés :vérification, canaux FIFO à pertes, automates temporisés
Encadreurs: Nathalie Bertrand (nathalie.bertrand@irisa.fr)
Description : Les protocoles de communication asynchrones sont classiquement modélisés par des automates communiquant par des files de messages FIFO. Une variante, les automates communicants à pertes (ou Lossy Channel Systems) permet de prendre en compte la non-fiabilité des canaux de communication et en particulier les pertes possibles de messages lors de leur transit [1,2]. L'utilisation de ce type de modèle pour représenter des protocoles réels de communication fait néanmoins abstraction de plusieurs aspects des protocoles, dont les contraintes temps-réel (délais de garde essentiellement).

Ce stage a pour objectif de définir et d'étudier une extension du modèle des Lossy Channel Systems avec horloges pour permettre de tenir compte des aspect temporisés des protocoles de communication. Ce modèle s'inspirera naturellement de la sémantique des automates temporisés [3], et de celle des Lossy Channel Systems. On s'intéressera alors logiquement à des questions d'expressivité, et de décidabilité pour différentes problèmes : vérification de propriété d'accessibilité, de sûreté, de vivacité... Une continuation naturelle sera de considérer des variantes probabilistes du modèle obtenu, et de développer des techniques de vérification généralisant celles dédiées aux Lossy Channel Systems avec pertes probabilistes [4,5].
Bibliographie :

Timed rational graphs
Mots clés : Rational graphs, Timed systems, Languages, Logic.
Encadreurs: Christophe Morvan (christophe.morvan@irisa.fr). Projet VerTeCs, tel 02-99-84-25-15, F 207, and Valentin Goranko, Technical University of Denmark, Department of Informatics and Mathematical Modelling (vfgo@imm.dtu.dk)
Description : Rational graphs [1] are a very expressive family of infinite graphs. They characterise context-sensitive languages and model various systems like pushdown systems, Petri nets, or HMSC. Unlike many of these systems, rational graphs are closed under synchronous product. This property is a potent tool in order to combine graphs without expending the complexity of the model.
A classical extension of finite models is performed adding a time dimension. The infinite state systems resulting from such an addition have been deeply studied since [2]. They clearly extend the initial finite model. For infinite state systems, the benefit from such an addition is not always obvious. In particular, for discrete time, one can simply define a rational tree (a rational graph which is a tree, see [3]) modelling time elapsing. Then, performing a synchronised product with any rational graph, produces a timed version of this graph. From previous observation, such a graph is still rational.
In this work, timed extension of rational graphs will be examined. Connection with timed extension of other infinite state systems will be studied (like timed pushdown automata [4], or time Petri nets [5]). It will be performed under the joint supervision of Christophe Morvan (Irisa) and Valentin Goranko (Technical University of Denmark).

Bibliography :
1. C. Morvan : On rational graphs, Fossacs 2000. LNCS 1784 pp. 252 - 266
2. R. Alur, D. Dill : A Theory of Timed Automata, Theoretical Computer Science (1994)
3. A. Carayol, C. Morvan : On rational trees, CSL 2006. LNCS 4207
4. Z. Dang, O.H. Ibarra, T. Bultan, R.A. Kemmerer, J. Su : Binary reachability analysis of discrete pushdown timed automata CAV 2000
5. P. M Merlin : A study of the recoverability of computing systems, PhD, 1974. University of California, Irvine.
Assurer / préserver les propriétés de disponibilitédans des systèmes d'informations
Mots clés : Sécurité, disponibilité, Système à événements discrets, Automates, Théorie du contrôle.
Encadreurs: Hervé Marchand (projet VerTeCs, tel 02 99 84 75 09, Bureau F201)
Description : La validation de politique de sécurité connaît un développement important depuis quelques années. L'engouement pour de telles recherches suit naturellement l'explosion du nombre de services proposés tant sur les systèmes mobiles et embarqués que sur le réseau Internet. En effet, ces derniers sont ouverts par nature et donc vulnérables aux attaques de pirates informatiques. Pour de tels services, la corruption de données ou la fuite d'information peut s'avérer catastrophique. Des notions de validation et de certification du niveau de sécurité des applications critiques [1] sont donc cruciales dans ce domaine. Dans ce contexte, ce stage a pour objectif d'étudier l'utilisation des méthodes formelles pour le déploiement automatique de contrôleurs les mettant en oeuvre.
En se basant sur des modèles d'automates et ses extensions ( à variables, temporisés, etc), on s'intéressera au déploiement de politique de sécurité modélisant des propriétés de disponibilité qui regroupent des notions de vivacité du système, contraintes temporisées, qualité de service, etc. Le problème ici sera de trouver une modélisation formelle adéquate permettant de spécifier ce type de propriétés [4,5] et d'adapter les techniques existantes de déploiement automatique [2,3] pour ce type de politiques de sécurité. On étudiera également la préservation de la validité des politiques de sécurité (notamment de disponibilité et de confidentialité) par composition (se doter d'un contrôle d'accès mettant en oeuvre une propriété de disponibilité peut en effet créer de nouvelles possibilités de fuites d'information et ainsi remettre en cause une propriété de confidentialité jusque là valide).
Bibliographie :
- [1] M. Bishop, Introduction to computer security. Addison-Wesley Professional, 2004
- [2] J. Dubreil, Ph. Darondeau, H. Marchand. Opacity Enforcing Control Synthesis. In Workshop on Discrete Event Systems, WODES'08, Gothenburg, Sweden, March 2008.
- [3] F. Cassez, J. Dubreil, H. Marchand. Dynamic Observers for the Synthesis of Opaque Systems. In 7th International Symposium on Automated Technology for Verification and Analysis (ATVA'09), Macao SAR, China, October 2009.
- [4] Y. Falcone, J-C. Fernandez, L. Mounier. Enforcement Monitoring wrt. the Safety-Progress Classification of Properties. In SAC'09: 24th Annual ACM Symposium on Applied Computing - Software Verification and Testing Track
- [5] KG. Larsen. modal specification. In Automatic Verification Methods for Finite State Systems, pp 232-246, 1989