Une tentative d'utilisation conjointe d'UML et d'une méthode formelle pour la modélisation de la sécurité des aéroports

The framework of this paper is the EDEMOI project whose aim is to model airport security. This approach involves the production of a graphi cal model (a set of UML class diagrams), to support the validation activity, and a formalmodel for verification purposes. In order to make sure that what is validated is also what is verifi ed, a strong link must exist between both models. RoZ offers a solution to this problem by transla ting annotated UML diagrams into Z specification. This paper presents the application of the R oZ tool to the model of the EDEMOI project and lists the problems faced during this translatio n approach.