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] M. Nilsson : Regular Model Checking, Ph.D. Thesis, 2005.
- [2] C. Morvan : On rational graphs, Fossacs 2000. LNCS 1784 pp. 252 - 266
- [3] A. Blumensath, E. Grädel : Automatic Structures. LICS 2000, pp. 51-62.
- [4] A. Carayol, C. Morvan : On rational trees, CSL 2006. LNCS 4207
- [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] 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 :
Sampath, R Sengupta, S Lafortune, K Sinnamohideen, D. Teneketzis. Diagnosability of discrete-event systems IEEE Transactions on Automatic Control, Vol 40, No 9, sept 1995
Shengbing Jiang, Ratnesh Kumar. Failure diagnosis of discrete-event systems with linear-time temporal logic specifications, in IEEE Transactions on Automatic Control, Vol. 49, Nr 6, pp 934- 945, June 2004
Olivier Contant, Stéphane Lafortune, Demosthenis Teneketzis. Diagnosis of Intermittent Faults in Discrete Event Systems; Theory and Applications, 14, 171-202, 2004. Kluwer Academic Publishers.
T. Jéron, H. Marchand, S. Pinchinat, M-O. Cordier. Supervision Patterns in Discrete Event Systems Diagnosis, in Workshop on Discrete Event Systems, WODES'06, Ann-Arbor (MI, USA), July 2006.
-
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 :
[1] A. Finkel. Decidability of the termination problem for completely specified protocols. Distributed Computing, 7(3) pp. 129?135, 1994.
[2] P. A. Abdulla and B. Jonsson. Verifying programs with unreliable channels. Information and Computation, 127(2), pp. 91?101, 1996.
[3] R. Alur, D. Dill. A Theory of Timed Automata. Theoretical Computer Science 126(2), pp. 183-235, 1994.
[4] P. A. Abdulla, N. Bertrand, A. Rabinovich, and Ph. Schnoebelen. Verification of probabilistic systems with faulty communication. Information and Computation, 202(2), pp. 141?165, 2005.
[5] C. Baier, N. Bertrand, and Ph. Schnoebelen. Symbolic verification of communicating systems with probabilistic message losses : liveness and fairness. In Proc. FORTE ?06, volume 4229 of Lecture Notes in Computer Science, pp. 212?227. Springer, 2006.
-
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 :
-
C. Morvan : On rational graphs, Fossacs 2000. LNCS 1784 pp. 252 - 266
-
R. Alur, D. Dill : A Theory of Timed Automata, Theoretical Computer
Science (1994)
-
A. Carayol, C. Morvan : On rational trees, CSL 2006. LNCS 4207
-
Z. Dang, O.H. Ibarra, T. Bultan, R.A. Kemmerer, J. Su : Binary
reachability analysis of discrete pushdown timed automata CAV 2000
-
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