Méthodes formelles pour la modélisation géométrique à base topologique (définitions et algorithmes avec la méthode B)

a méthode B est un langage de spécifications formelles largement utilisé pour le développement de logiciels critiques. Nous l'avons utilisée pour concevoir des logiciels complexes, appelés modeleurs géométriques, qui rendent possible la manipulation et la création des images de synthèses. Notre travail de formalisation et de preuve d'un noyau de modeleur géométrique à base topologique et d'une opération topologique réputée difficile permettant d'arrondir un objet, a montré les limites et les difficultés d'une approche consistant à traduire de manie re quasi-syntaxique en B les définitions mathématiques existantes. Néanmoins, nous avons proposé une autre approche fondée sur une extension de la méthode B appelée B événementiel. Nous l'avons expérimenté avec succès sur un algorithme permettant de construire la subdivision du plan induite par un ensemble de droites. En conclusion, la méthode B semble être adaptée à la modélisation géométrique : l'expérience est donc à poursuivre.The B method is a formal specification language used in order to develop critical systems. We used this language to develop complex softwares called modellers. These softwares allow to handle and create computer-generated images.Our work consists in the formalization and the proof of a topology-based modeller kernel and of a complex operation which is the topological part of the rounding operation. It teaches us the limits and difficulties of the approach which consists in translating mathematical definitions directly into formal specifications. Nevertheless, we proposed another approach based on an extension of the B method called event B. We used it successfully to specify a geometrical algorithm which calculates the subdivision of the plan corresponding to a set of lines. In conclusion, the method B seems to be adapted to geometric modelling: the experience deserves to be continued.EVRY-BU (912282101) / SudocSudocFranceF