Abstract FR:

L'objet de ce travail a été de modéliser différents aspects de deux méthodes semi-formelles: la méthode de développement de Jackson (JSD) et la méthode de programmation de Jackson (JSP). Nous présentons d'abord les caractéristiques des méthodes formelles pour en déduire un schéma de modélisation de méthodes. Ce schéma est appliqué, dans son intégralité, à la méthode de programmation, c'est-à-dire que nous proposons une expression formelle des objets manipules, un principe de validation des programmes ainsi qu'un principe pour leur synthèse. Nous étudions ensuite la mise en œuvre de la méthode ainsi modélisée, son automatisation, ainsi que les stratégies de décomposition qui sont proposées dans la méthode originale. Puis nous en proposons une formalisation dans le langage DEVA. La dernière partie concerne l'extension des notions précédentes au parallélisme. Nous proposons une sémantique opérationnelle pour les réseaux de processus manipules par la méthode de développement, grâce à laquelle les opérations de décomposition parallèle de la méthode de programmation ont également pu être formalisées. Enfin, nous en déduisons un schéma de validation et de transformation pour l'implémentation de ces réseaux.