Les systèmes interactifs sont des systèmes informatiques qui échangent avec un utilisateur humain. Ils peuvent être décrits grâce à un UIDL (User Interface Description Language). Nous cherchons à apporter des garanties sur de tels systèmes. À cette fin, nous voulons exprimer et vérifier formellement des propriétés qui portent sur des aspects interactifs de programmes décrits à l'aide d'un UIDL. Nous disposons pour cela d'un UIDL formel, BIGUIL, dont la sémantique est décrite à l'aide des bigraphes. Nous voulons explorer l'outillage de BIGUIL pour garantir ces propriétés par construction.