Ce cours peut être vu comme un complément du cours sur UML. UML est un ensemble de notations que l'on peut qualifier de semi-formel. UML est un standard permettant les approches à objets. Il existe des outils riches extensibles et conviviaux le mettant en oeuvre, et du fait de sa normalisation, son utilisation est indispensable comme outil de structuration et comme outil de communication dans l'entreprise.
Il présente toutefois des limitations. S'il est suffisant pour des processus de validation (montrer que le système répond aux besoins) informels, il n'offre guère de possibilités pour une vérification formelle de propriétés spécifiques (montrer qúun signal arrivera toujours avant un autre par exemple).
Les diagrammes UML de base même s'ils permettent une certaine description de la dynamique des objets par l'intermédiaire des diagrammes d'états, des diagramme d'activité, des diagrammes de séquence, des diagrammes de collaboration sont insuffisants pour aborder les systèmes temps réel et les systèmes embarqués. En effet, ils proposent des visions parcellaires de la dynamique des systèmes : ou bien on décrit les changements d'état dans un objet, ou bien on représente un dialogue entre les objets lors d'un scénario bien particulier. Or le besoin d'une vue d'ensemble (au niveau système) de toutes les interactions et de tous les scénarios est souvent indispensable pour les évaluations de performance et de sécurité. Tout scénario pouvant mener à des situations redoutées doit en particulier pouvoir être généré. En d'autres termes, il est souvent nécessaire de montrer que le comportement interne des objets est compatibles avec les diagrammes de séquence et de collaboration et surtout que l'entrelacement de plusieurs diagrammes de séquence ne peut pas avoir des conséquences dommageables. Les diagrammes d'états exprimées sous la forme des ``StateCharts'' sont les plus proche des besoins. Toutefois ils sont fondés sur une communication synchrone entre les tâches ce qui n'est pas réaliste dans le cas de systèmes distribués.
Une autre limite de UML est que rien n'est offert pour évaluer les performances du système que l'on est en train de spécifier et de concevoir. De même, il n'est pas possible de prouver formellement que certaines situations ne seront jamais atteintes (``safety'' c'est-à-dire sûreté), ni que certains états pourront toujours être atteints si cela est nécessaire (``liveness'' c'est-à-dire vivacité), compte tenu des contraintes temporelles. Des compléments des outils UML permettant la simulation sont actuellement offerts, mais une simulation n'est pas une preuve formelle. Encore une fois elle ne fournit qúune vision parcellaire. Enfin, rien n'est offert pour les études de disponibilité et de fiabilité, c'est-à-dire permettant la prise en compte quantitative des possibilité de défaillance de certains éléments. Pour le moment, dans l'industrie, de telles études sont menées en parallèle avec les équipes développant les logiciels, avec une autre modélisation fonctionnelle et rien n'assure la cohérence avec les deux points de vue. L'outil MISS-RdP (IXI) fondé sur les réseaux de Petri est utilisé dans ce contexte.
Les réseaux de Petri ne sont pas une norme industrielle comme UML. Il s'agit d'un modèle formel. Le but du cours n'est donc pas de permettre un entraînement à l'utilisation d'un outil largement utilisé dans l'industrie. Il est de sensibiliser à une méthode formelle, de montrer sa complémentarité vis-à-vis des outils semi-formels, les avantages que l'on peut en retirer, mais aussi les difficultés rencontrées. Ces difficultés expliquent la lenteur de leur diffusion dans le milieu industriel (vous pourrez toutefois remarquer que certaines notations UML se rapprochent déjà de certains concepts formels). Toutefois, vu l'accroissement continu de la complexité des systèmes informatiques (au sens application et non système d'exploitation), vu les enjeux économiques qúils impliquent et les risques industriels qui en sont la conséquence, il est fort probable que l'utilisation des méthodes formelles ne pourra pas être indéfiniment repoussée. Il s'agit donc de vous préparer à ce changement.
Quelques pointeurs (octobre 1999):