%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %\subsection{Thèmes de recherche} Les systèmes développés de nos jours sont de plus en plus complexes et leur fonctionnement peut avoir des conséquences importantes sur leur environnement, voire irréversibles : systèmes avioniques, médicaux \ldots Il est par conséquent indispensable d'obtenir des systèmes sûrs, dont le fonctionnement a pu être vérifié avant leur mise en \oe uvre. \\ La spécification d'un système présente tout d'abord des avantages quant à la description et la compréhension du système considéré : \begin{itemize} \item L'écriture de la spécification permet au concepteur de mieux comprendre le fonctionnement attendu de son système ainsi que les interactions entre les différents composants. L'écriture du modèle conduit à remettre en cause des choix conceptuels d'une part et à une meilleure compréhension du système développé d'autre part. \item Le modèle constitue une documentation précise lors de la maintenance. \end{itemize} \bigskip De plus, les modèles formels permettent de prouver formellement (i.e.\ mathématiquement) le bon fonctionnement du système développé. On est alors complètement sûr que quelle que soit l'évolution du système, son comportement sera celui attendu. Outre les avantages précédents, propres à la spécification, les méthodes formelles offrent des outils d'analyse du système modélisé : \begin{itemize} \item La simulation permet de se convaincre du bon fonctionnement du système, ou éventuellement de découvrir quelques erreurs. Leur correction à ce stade est peu coûteuse, comparée à celle d'un système déjà mis en \oe uvre (que ce soit avec des moyens logiciels ou matériels). \item La vérification exhaustive du comportement du système. On applique dans un premier temps des techniques de simulation pour effectuer un débogage grossier, puis le modèle est affiné lors de la vérification des propriétés souhaitées. \end{itemize} \bigskip Les activités de la thématique \emph{spécification et vérification} s'articulent autour de plusieurs axes de recherche : \begin{itemize} \item La méthodologie de développement d'une spécification : quel modèle/langage choisir, à quel niveau d'abstraction se placer, comment considérer le problème, comment commencer à écrire et développer la spécification. \item Les systèmes à modéliser étant en général de taille assez conséquente, ils sont spécifiés de manière structurée, par exemple avec une architecture modulaire. L'analyse modulaire vise à tirer parti de cette structuration pour repousser les limites des techniques d'analyse de propriétés. \item Lorsqu'une spécification a été validée à un niveau abstrait, des détails peuvent être introduits par un processus de raffinement. La vérification du modèle raffiné doit alors s'appuyer sur celle du modèle abstrait. \item Enfin, l'utilisation de prouveurs de théorèmes permet de valider les étapes de raffinement de modèles. L'utilisation de ces prouveurs pour des problèmes numériques devra à terme permettre d'aborder des propriétés de systèmes en temps continu. \end{itemize} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \subsubsection{Méthodologie de spécification} Si l'utilité et la nécessité des spécifications formelles est bien démontrée dès qu'il s'agit de développer ou de manipuler des logiciels complexes, écrire les spécifications d'un système demeure une tâche ardue et délicate. Nous explorons ici comment rendre ce travail plus aisé en fournissant des lignes guide, soit pour écrire directement la spécification, soit en utilisant un langage ou un formalisme intermédiaire plus accessible, ou encore en s'appuyant sur des schémas identifiés (pour cette dernière approche, le lien avec les étapes ultérieures de développement est également étudié). Ce travail de méthodologie a tout d'abord eu pour but de fournir des spécifications écrites dans le langage de spécification algébrique \textsc{Casl}, ou dans une extension \textsc{Casl-Ltl} \cite{Reggio:2003:CLC} pour les systèmes dynamiques. % Mais les idées alors développées sont assez générales pour trouver leur application dans l'écriture de spécifications dans d'autres langages (Z, LOTOS, réseaux de Petri, RAISE). Dans \cite{ChoppyReggioJLAP06} des lignes guide sont proposées pour l'écriture de spécifications de systèmes dynamiques (simples ou structurés) ainsi que de types de données. Différentes caractéristiques constitutives d'un système sont mises en évidence et les propriétés à rechercher sont détaillées. Le lien de cette méthode avec les cas d'utilisation (qui sont munis d'une description structurée) est décrit dans \cite{ChoppyReggioFASE04}, ce qui permet de fournir une graphique familière aux utilisateurs de la notation UML. Il existe des «~patterns~» pour décrire les problèmes, ce sont les «~Problem Frames~» de Michael Jackson. Afin de bénéficier des concepts structurants des problem frames (et aussi de leur graphique) nous avons travaillé pour les intégrer dans une démarche de spécification, ce qui nous a conduit à les équiper d'une description plus détaillée proposée en UML à laquelle nous savons associer une spécification formelle \cite{ChoppyReggioIWAAPF04,ChoppyReggioIASSE04,ChoppyReggioIST05}. Ces travaux nous ont aussi conduit à proposer des schémas de problème plus complexes adaptées toutefois à des larges classes d'application \cite{ChoppyReggioIST05,ChoppyReggioASWEC06}. Les «~patterns~» ont d'abord été proposés pour des étapes ultérieures du développement, aussi avons nous exploré comment faire le lien entre une démarche de spécification utilisant les problem frames et un développement à l'aide de styles d'architecture \cite{ChoppyHeiselWADT}, et nous avons proposé dans \cite{ChoppyHeisel04a} une approche pour les systèmes d'information, puis dans \cite{ChoppyHatHeisIE05,ChoppyHatHeisAPSEC06} une approche plus générale, dans les deux cas produisant une architecture par composants. Nous souhaitions mettre en \oe uvre pour d'autres formalismes les idées proposées dans \cite{ChoppyReggioJLAP06} pour l'écriture de spécification, et nous avons donc exploré dans \cite{CC-LP-CPN-04} l'écriture de réseaux de Petri. Ces travaux ont été poursuivis dans le cadre d'un stage de Master Recherche en 2006. Dans \cite{CC-LP-MeFo-06,LP-MeFo-06,CC-SH-HK-FK-LP-YTM-ICTAC-06}, %CC il faut mettre les chapitres MeFoSyLoMa-06, nous présentons des idées générales sur les critères qui interviennent dans l'écriture des spécifications, et sur certains des travaux présentés ci-dessus. Il est important de noter que chaque méthode de spécification est plus ou moins adaptée à un problème spécifique. C'est pourquoi, il faut tirer parti au mieux des différentes techniques existantes~\cite{FK-LP-DSO-06}. L'utilisation conjointe de différents outils est nécessaire. Pour atteindre un tel objectif, nous sommes impliqués dans le processus de normalisation des réseaux de Petri~\cite{FK-LP-NWI-04, LH-FK-LP-NT-PNML-05, LH-FK-LP-NT-FORTE-06}. Les réseaux de Petri sont normalisés ISO/IEC 15909-1 (première partie d'une norme en 3 volets). Les aspects pratiques concernant un format d'échange (ISO/IEC 15909-2) sont en cours. Ils impliquent la définition d'un métamodèle. Ceci a permis d'automatiser la lecture/écriture d'un fichier écrit en PNML (Petri Net Markup Language) en utilisant une approche MDA (\emph{Model-Driven Architecture}). Le langage PNML a également évolué au cours de ces travaux. De plus, nous avons soumis un addendum à la partie 1 de la norme pour définir les réseaux symétriques, qui sont des réseaux de haut niveau simples, et servent de base aux travaux sur la partie 2. Enfin, les travaux de la partie $3$, portant sur les extensions de réseaux de Petri, viennent de démarrer. Nous sommes éditeurs de ce volet de la norme. \subsubsection{Vérification Modulaire} Nous nous intéressons ici tout particulièrement à des systèmes complexes, parallèles, asynchrones, modélisés à l'aide de réseaux de Petri. La principale méthode de vérification de propriétés à partir d'un modèle spécifié par un réseau de Petri consiste en l'exploration du \emph{graphe d'états accessibles}. Toutefois, pour des systèmes de taille importante, on se heurte très rapidement au «~problème de l'explosion combinatoire de l'espace d'états~». Le graphe d'états est alors trop gros pour être stocké en mémoire. De nombreuses techniques ont été proposées pour pallier ce problème (ordres partiels, bit-state, \ldots). Nos travaux se concentrent sur l'analyse modulaire qui tire parti de la structure modulaire du modèle à analyser. L'activité des modules est explorée de manière indépendante plutôt qu'entrelacée. La technique de graphes d'états modulaires que nous développons consiste alors à construire un graphe d'états «~local~» par module plus une structure appelée «~graphe de synchronisation~» décrivant les interactions entre les différents modules~\cite{invLP-ISPS-05}. \\ Nous avons proposé, dans~\cite{CL-LP-ACSD04}, des algorithmes effectuant la construction du graphe d'états modulaire d'un réseau de Petri, ainsi que la vérification de propriétés (bornes, blocage, vivacité, \ldots). L'implémentation d'un prototype a permis de réaliser des expérimentations sur un problème classique d'automates industriels (les véhicules autoguidés). Les résultats ainsi obtenus ont montré des gains considérables --- passage de 31.000.000 à 900 états. Toutefois, des études de cas ont été menées dans~\cite{LP-PNNL-05}, qui montrent que la technique est particulièrement adaptée à des systèmes composés de sous-systèmes autonomes faiblement couplés tels que ceux considérés en automatique. Dans le pire des cas, lorsque les sous-systèmes sont totalement synchronisés, on aboutit à un léger surcoût. \\ Nous avons adapté cette approche à la synthèse de réseaux de Petri, en collaboration avec Philiipe {\sc Darondeau} de l'IRISA~\cite{Darondeau-Petrucci}. \\ Suite aux résultats encourageants de la technique de graphes d'états modulaires, nous l'avons étendue à des modèles de réseaux de Petri comportant une modélisation du temps. Nous nous sommes intéressés à la fois aux réseaux temporisés, dans lesquels on considère une horloge globale et les jetons sont estampillés par la date à laquelle ils sont prêts, et aux réseaux temporels, où le temps est compté localement, un intervalle est associé à chaque transition et indique la période dans laquelle la transition doit être franchie, à partir du moment où toutes ses préconditions sont satisfaites. Nous avons donné, dans~\cite{CL-LP-CPN-05, CL-LP-STTT-06}, des algorithmes de construction de graphe d'états modulaires pour les réseaux temporisés. L'inconvénient majeur réside dans l'utilisation de l'horloge globale. En effet les états du graphe sont des couples (marquage, date). Lorsque le système peut évoluer indéfiniment, le graphe obtenu est alors infini. Dans~\cite{SM-LP-MOCA-06}, une technique similaire est présentée pour les réseaux temporels. Les états du graphe sont composés d'un marquage et d'une vecteur de valuations temporelles associées aux transitions. Le graphe obtenu est alors fini (si le réseau de Petri est borné). Ces différents algorithmes ont été implémentés, et des expérimentations~\cite{CL-LP-STTT-06} ont montré les apports de l'approche. une autre approche est l'analyse compositionnelle, qui consiste à vérifer des propriétés d'un sous-système pour valider celles du système complet. Nous avons développé un tel algorithme pour le vérification de formules {\sc ltl$\setminus$x}~\cite{KK-LP-MR-FORTE-07}. \subsubsection{Raffinement de spécifications de haut niveau} De nos jours, les systèmes à modéliser et à analyser sont de taille de plus en plus grande. Pour s'affranchir des problèmes inhérents à l'explosion du nombre d'états, une spécification est souvent développée pas à pas (ce qui correspond à une démarche classique de développement de génie logiciel). Tout d'abord, un modèle abstrait est défini. Une fois que ses propriétés sont vérifiées, une étape de raffinement, qui introduit un niveau de détail supplémentaire, peut être effectuée. Un tel ajout peut préciser la description de l'actuel fonctionnement d'une partie du système, ou introduire une partie supplémentaire. Le modèle ainsi raffiné est ensuite vérifié. Une nouvelle étape de raffinement peut alors être appliquée, et ce jusqu'à atteindre un niveau suffisant de description. Trois types de raffinement ont été introduits par Lakos et Lewis, pour les réseaux de Petri de haut niveau : le raffinement de sous-réseau, le raffinement de n\oe{}ud et le raffinement de type. Ces raffinements ont été utilisés dans le cadre d'une approche incrémentale à la spécification de systèmes complexes. Outre les avantages du raffinement pour la spécification de systèmes, ils permettent de faciliter la vérification de propriétés. En effet, d'une part certaines propriétés sont préservées par le raffinement, et d'autre part, l'analyse du modèle abstrait permet de guider celle du modèle concret, économisant ainsi en temps de calcul et espace mémoire lors de la construction de graphes d'états. Jusqu'à présent, le processus de raffinement de réseaux est complètement manuel. La vérification des contraintes peut être assez complexe. Par conséquent, nous souhaitons prouver automatiquement qu'un réseau est effectivement un raffinement d'un autre réseau (abstrait). Pour cela, nous utilisons des techniques de preuve de théorèmes, en particulier, l'assistant d'aide à la preuve Coq, développé à l'\acs{Inria}. Nous proposons donc une formalisation en Coq des définitions de raffinements ainsi que des réseaux auxquels ils s'appliquent. Ceci a tout d'abord été développé pour les raffinements de sous-réseaux et de n\oe uds des réseaux places/transitions, et appliqué à quelques exemples. Ce travail est étendu, dans le cadre d'un stage de master, aux réseaux colorés. Le raffinement de types pour les réseaux de Petri de haut niveau a été peu étudié. Pour développer cet aspect, nous nous sommes intéressés dans un premier temps à la vérification de systèmes paramétrés. Le bon fonctionnement de la famille de protocoles «~stop-and-wait~» a ainsi pu être vérifié~\cite{JB-GG-LP-MOMPES-05,JB-GG-LP-NJC-05}, et ce, de manière paramétrée. %Utiliser ce processus de raffinement offre plusieurs avantages. Il permet de %commencer avec un modèle plus abstrait et donne une meilleure vision, plus %structurée, du système à l'étude. Les composants sont clairement identifiés %et le processus de modélisation est aisé. Le processus de validation devient %lui aussi plus facile: les propriétés du système sont contrôlées à chaque %étape. Ainsi des modèles abstraits sont validés avant ajout de nouveaux %détails. De plus, l'analyse d'un modèle concret complet peut ne pas être %raisonnable, en raison de sa taille. Un raffinement aide à faire face à ce %problème dans la mesure où il peut préserver certaines propriétés ou certains %résultats d'analyse obtenus grâce au modèle raffiné. %Nous nous proposons ici de prouver formellement, c'est-à-dire en utilisant %un système de preuve, la correction de chaque étape de raffinement. Trois %types de raffinement sont concernés: le raffinement de sous-réseau, le %raffinement de n\oe{}ud et le raffinement de type. Une première spécification %et preuve a été faite dans Coq~\cite{} concernant les deux premiers %raffinements. \subsubsection{Spécifications et preuves formelles} Dans le cadre du nouveau projet CerPAN~\footnote{\url{http://www-lipn.univ-paris13.fr/CerPAN/}} (Certification de Programmes d'Analyse Numérique, ANR décembre 2005), nous nous intéressons au développement et à la mise en application des méthodes permettant de démontrer formellement la correction de programmes issus du domaine de l'analyse numérique. Le projet concerne plus particulièrement des programmes apparaissant de manière récurrente dans la résolution de problèmes critiques. Beaucoup de programmes critiques sont issus de ce domaine, mais les travaux traitant directement des applications des méthodes formelles aux programmes d'analyse numérique sont rares. La principale raison est l'utilisation intensive des nombres réels (à virgule flottante) dans les programmes numériques, alors que les méthodes formelles manipulent plutôt des nombres entiers, ou plus généralement des structures discrètes. Deux méthodes sont explorées dans ce projet, toutes deux étant vouées à être mises en pratique sur une étude de cas (gradient analytique). \begin{enumerate} \item L'une consiste à utiliser des outils de vérification de programmes tels que Why et Caduceus (dédié aux programmes C) développés au \acs{LRI}. Il s'agit de travailler sur un programme déjà existant, qui va être annoté suivant les propriétés à préserver. Ces annotations engendrent alors des obligations de preuve pour divers systèmes de preuve formelle (Coq, PVS, Isabelle/HOL, HOL 4, HOL Light, Mizar,...). Ces outils de vérification de programmes ne traitaient pas les nombres flottants. Nous avons donc participé aux phases de décision concernant l'extension de ces outils aux nombres flottants sous forme d'un langage de spécification pour les propriétés relatives aux nombres à virgule flottante. Ces ajouts sont distribués avec le système. \item L'autre méthode consiste à effectuer la formalisation et la preuve du problème correspondant au programme ou à l'algorithme étudié, puis à utiliser le mécanisme d'extraction du système Coq afin d'obtenir automatiquement un programme prouvé correct. Ce principe d'extraction ne traite pas non plus la famille des nombres réels. Nous avons commencé par décider d'extraire vers des réels exacts et non vers des nombres flottants et nous sommes actuellement en train de rechercher un modèle adéquat de réels exacts (réaliste d'un point de vue implantatoire, efficace, ...) pour étendre l'extraction de Coq. \end{enumerate} Nous essayons de tenir compte des aspects d'efficacité qui peuvent jouer un rôle déterminant dans le domaine de l'analyse numérique en particulier. Les méthodes développées dans ce projet auront un large champ d'application dans les environnements destinés à produire du code numérique garanti correct par rapport à des spécifications formelles et devra à terme permettre d'aborder des propriétés de systèmes en temps continu lors d'étapes de raffinement.\\ Nous avons développé une procédure de décision dans Coq pour les corps algébriquement clos~\cite{DD-MM-Calculemus2005}. Cette procédure de décision est basée sur la méthode d'élimination des quantificateurs et utilise l'interface~\cite{DD-MM-JSC} que nous avons développée entre le prouveur Coq et l'outil de calcul formel Maple. Nous avons effectué en Coq la preuve du $20^{\mbox{\small ème}}$ problème de Diophante (l'aire d'un triangle rectangle dont les côtés sont mesurés par des entiers peut-elle être un carré parfait?). Ce problème fut résolu négativement par Fermat au moyen de la méthode de descente infinie. La méthode de descente infinie permit à Fermat de prouver le théorème pour $n=4$. Nous avons formalisé cette preuve en Coq. Nous proposons une méthodologie pour détecter efficacement les erreurs sur des composants matériel génériques (SoC), utilisant à la fois des techniques de model-checking, de test et des prouveurs de théorèmes. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \subsection{Perspectives de recherche} \subsubsection{Méthodologie de spécification} Les idées développées dans \cite{ChoppyReggioJLAP06} peuvent être reprises et adaptées en fonction des langages de spécification formelle cibles. Des travaux ont été entamés notamment en direction : \begin{itemize} \item du langage Raise/RSL, en collaboration avec Anne Haxthausen qui est experte de ce langage et qui, à l'occasion du développement d'études de cas, a mené une réflexion sur les aspects méthodologie (sans l'avoir formalisée en tant que telle). \item des réseaux de Petri, pour lesquels, à la suite de~\cite{CC-LP-CPN-04}, des travaux ont été % entamés d'une part à l'occasion d'un stage de master recherche, et d'autre part poursuivis en collaboration avec Gianna Reggio, pour les réseaux places/transitions~\cite{CC-LP-GR06r}, pour les réseaux colorés~\cite{CC-LP-GR07r}, et seront étendus aux réseaux hiérarchiques, puis temporisés. \end{itemize} Ces travaux vont nous permettre d'identifier une partie ``générique'' indépendante du formalisme cible, et une partie spécifique induite par le choix du type de modèle. \subsubsection{Vérification modulaire et distribuée} \begin{itemize} \item Vérification modulaire temporisée : les travaux menés jusqu'à présent permettent la construction d'un graphe d'états modulaire pour des modèles de réseaux de Petri avec contraintes de temps. Toutefois, l'intérêt de l'approche est de pouvoir vérifier les propriétés du réseau de Petri sans avoir à déplier le graphe modulaire. \item Etudes de cas : les techniques développées seront appliquées à des exemples complexes. Nous avons entamé cette démarche en utilisant le «~fieldbus protocol~». \item Vérification distribuée : dans~\cite{LK-LP-ICATPN04}, nous avons présenté une implémentation distribuée du calcul de graphe d'états. Nous avons également montré comment les propriétés simples d'un réseau de Petri peuvent être vérifiées. L'analyse de propriétés plus élaborées telles que la vivacité est plus complexe. De plus, nous souhaitons utiliser un cluster de machines mis en place récemment au \acs{LIPN} pour pouvoir implémenter une plateforme distribuée et effectuer des tests. Cela nous permettra en particulier d'évaluer la répartition des n\oe uds du graphe sur les différents processeurs. À terme, l'architecture logicielle devra également permettre la construction distribuée du graphe modulaire. \item Heuristiques pour la construction de graphes d'états : nous avons soumis un projet de «~discovery grant~» à l'\acs{ARC} (Australian Research Council), HAVOCS (Heuristic Approaches to the Verification Of Complex concurrent Systems~»). L'objectif est d'utiliser des approches heuristiques (telles que les algorithmes fourmis) pour guider la génération du graphe d'états. Cette politique de construction devra rechercher en priorité des chemins pouvant conduire à des états invalidant une propriété souhaitée. Ce travail sera effectué en collaboration avec Hanene Azzag de l'équipe \acs{A3}. \end{itemize} \subsubsection{Raffinement} \begin{itemize} \item Les premières expériences effectuées avec le prouveur de théorèmes Coq pour montrer qu'un réseau de Petri places/transitions est un raffinement d'un autre ayant été probantes, nous souhaitons étendre ces travaux aux différents types de raffinements de réseaux de Petri colorés (stage de master recherche en cours). De plus, pour rendre ces travaux utilisables, il est nécessaire d'implémenter un outil faisant la traduction automatique d'un réseau de Petri en une spécification Coq. \item Parmi les raffinements proposés par Lakos et Lewis, on en distingue deux (raffinements de n\oe ud et de sous-réseau) qui portent sur la structure du réseau de Petri, et un (raffinement de type) qui s'intéresse aux données manipulées dans un réseau de haut niveau. La définition du raffinement de type est pour l'instant très limitée. Nous envisageons donc de l'étendre en nous inspirant des techniques d'abstraction de données et des travaux existant sur l'indépendance de données. \item Ces travaux seront appliqués à des études de cas, mettant ainsi en évidence les problèmes spécifiques que l'on peut rencontrer lors de tests à grande échelle. \end{itemize} \subsubsection{Autres activités} \begin{itemize} \item Collaboration avec l'\acs{ONERA} (coencadrement de thèse depuis février 2006) : modélisation de la reconnaissance de chroniques dans le cadre de simulations de systèmes distribués \cite{BCC-DX07,BCC-RJCIA07} \item Collaboration avec l'équipe \acs{A3} : modélisation et vérification du protocole de communication du systèmes multi-agents développé par Hager Karoui, à l'aide de réseaux de Petri de haut niveau. \item Standardisation : les travaux sur la norme ISO/IEC 15909 partie 2 concernant le format d'échange de réseaux de Petri seront poursuivis. Un des points cruciaux est la prise en compte d'extensions qui seront normalisées par la suite dans la partie 3 du standard, dont nous sommes porteurs. \end{itemize}