Méthodes formelles

23 Février 2020

Je cite souvent Hillel Wayne et il cite souvent les méthodes formelles. Pour expliquer ces concepts, j'ai décider d'apprendre à utiliser différentes méthodes légères pour modéliser un cas d'usage.

Deux concepts sont au cœur des méthodes formelles :

• La conception formelle : comment concevoir des fonctionnalités sans ambiguïté
• La vérification formelle : comment vérifier que les fonctionnalités n'ont pas d’ambiguïté

Les deux concepts sont très liés car on ne peut répondre qu'aux deux problèmes en même temps. Par contre, les deux fournissent des outils différents.

Pour illustrer les outils et leurs limitations, nous allons spécifier le cas d'usage suivant :

• Pour utiliser le service X, il faut que l'utilisateur ait vérifié son email
• Tout utilisateur peut changer son email
• Pour vérifier son email, l'utilisateur doit appeler le lien unique contenu dans l'email envoyé lors de son inscription
• Les emails venant du domaine gmail.com ne peuvent pas être vérifiés (disons que ce n'est pas la cible du service X)

Cette spécification est ambiguë car faite pour : https://www.hillelwayne.com/post/feature-interaction/

La table de vérité

Outil issu du domaine de la logique booléenne, la table de vérité est un outil très simple à appréhender les problèmes qui peuvent se réduire à des propositions logiques.

Lien envoyé	Email en gmail.com	Lien visité	Accès au service X
Non	Oui	X	Non
Non	Non	X	Non
Oui	Oui	Oui	Non
Oui	Non	Oui	Oui
Oui	Non	Non	Non
Oui	Oui	Non	Non

C'est la seule table de vérité que j'ai réussi à faire pour lever l'ambiguïté. En entrée (les trois premières colonnes), on note si la proposition est vraie ou fausse, et on entre dans la dernière colonne si l'accès au service est permis ou pas. Je me suis permis de réduire le tableau dans le cas où on n'envoie pas de lien, car dans ce cas, il n'est pas possible pour l'utilisateur de visiter le lien qui n'existe pas.

Les tables de vérité ont été popularisé par le philosophe et logicien Ludwig Wittgenstein. Elles sont un premier pas pour vérifier les spécifications. Bien que formellement correcte, l'ambiguïté de la spécification n'est pas levé par la table elle-même : de quel email parlons-nous quand on dit que gmail.com est interdit ? L'erreur peut encore se glisser dans le manque de clarté dans la définition des termes.

Le diagramme de flux

Le deuxième outil léger pour faire de la spécification formelle : les diagrammes de flux. Plutôt que de se concentrer sur un état fixe, on se concentre plutôt sur l'enchaînement des actions et des conditions. Les outils tels que DRAKON permettent ensuite de vérifier que de tels schémas sont cohérents, voire de générer du code à partir de ceux-ci. Attention DRAKON n'est pas un outil de graphes, mais bien de spécification. On peut valider le modèle contrairement aux outils de dessin qui permettent des graphes incorrects.

Les diagrammes ont une lisibilité et une facilité de compréhension sans pareil. Ils ont été conçus dans ce but et c'est une valeur sur pour explorer des processus métiers. On peut mieux saisir les contraintes temporelles, limiter les variables changeantes. Dans notre cas on peut lever facilement l'ambiguïté de la spécification en nommant un "Email To Verify" et un "Secondary Email".

Il est intéressant de voir que l'on peut rapidement exploser la complexité tout en restant clair sur les cas qui amène aux mêmes finalités. Alors que les tables de vérité peuvent vite devenir incompréhensibles au fur et mesure de l'augmentation du nombre de cas, il est plus facile de suivre un diagramme de flux, car les trajectoires sont tout de suite reconnues par notre œil habitué à ces motifs. Pour vous en convaincre, réaliser le tableau de vérité qui correspond à la séquence "User Inbox" de notre diagramme : vous vous retrouverez avec 3 entrées, 2 sorties et 8 lignes pour explorer tous les cas.

Le langage de spécification

Pour l'instant, nous n'avons utilisé que des outils de spécifications qui pourrait être fait sur papier rapidement. Nous allons à présent utiliser un langage de modélisation. Dans les outils de spécification, le langage de spécification est le plus avancé car il permet de fournir des vérifications très avancées et automatiques. Par exemple TLA+ peut explorer rapidement des problématiques pour évaluer des problèmes de concurrence. Pour notre cas, nous allons utiliser Alloy pour vérifier la validation des emails. Le langage se veut similaire de l'orienté objet et permet de produire des exemples et des contre-exemples aux contraintes que l'on fournit.

La logique de validation

Alloy étant difficile à saisir rapidement, nous allons spécifier chaque partie de la fonctionnalité itérativement.

open util/ordering[Service] // L'objet "Service" sera représenté par des états successifs

sig Email {}  // On définit le set d'emails
sig User {} // ainsi que les utilisateurs

// Pour chaque état du service
sig Service {
	live: set User, // on a un set d'utilisateurs utilisant le service
	verified: set User, // Le service aura un set d'utilisateurs vérifiés
	email: User -> one Email, // Pour chaque utilisateur il y a un email
} {
	verified in live // les utilisateurs vérifiés utilisent le service
	live = User // on ne s'intéresse qu'aux utilisateurs qui utilise le service
}

// Les relations d'utilisateurs à Email ne changent pas : L'utilisateur ne peut changer son Email
fact { all s, s': Service | s.email = s'.email }

// Un utilisateur vérifié restera toujours vérifié
fact { all s: Service, s': s.next | all u: s.live | u in s.verified => u in s'.verified }

// Exemple avec aucun utilisateur vérifié au départ et tous les utilisateurs véfifiés dans le dernier état
run { no first.verified && last.verified = User }

La commande run permet de demander à Alloy de générer des exemples de la spécification. L'aide visuelle est très pratique, on peut ainsi rapidement explorer les incohérences du modèle.

Exclusion des Emails en Gmail

Pour spécifier le fait que les emails peuvent être @gmail.com, on va étendre le set d'emails :

sig Gmail extends Email {}

Ensuite on introduit la notion de lien envoyé à l'utilisateur et qu'il ne sera validé que s'il n'est pas dans Gmail :

sig Service {
	live: set User,
	verified: set User,
	email: User -> one Email,
	link: User -> one Email
}

// ...

// Les utilisateurs ne peuvent pas changer de lien d'inscription
fact { all s, s': Service | s.link = s'.link }
// Les utilisateurs ne peuvent pas changer d'Email
fact { all s, s': Service | s.email = s'.email }
// si l'utilisateur est vérifié, son email `u.(s.email)` dans le précédent état n'appartient pas à Gmail
fact { all s: Service, s': s.next | all u: s'.verified | u.(s.email) in Email - Gmail }

Enfin on vérifie que notre modèle est correct :

check { all s: Service | all u: s.verified | u.(s.link) in Email - Gmail } for 3

Il est à noté qu'étant un vérificateur partiel, on ne peut faire des vérifications que pour un nombre limité de cas avec le mot clé for x (ici 3 instances de Service). On peut augmenter notre confiance dans le modèle en augmentant ce paramètre.

Possibilité de changer les Emails

Enfin, on peut rajouter à l'utilisateur la possibilité de changer d'email. On enlève la contrainte sur le modèle précédent et rajoutons la condition que l'utilisateur ne peut pas à la fois changer d'email et confirmer son email au même moment :

fact { all s: Service, s': s.next | all u: s'.verified | u in s.live - s.verified => u.(s.email) = u.(s'.email) }

On peut faire tourner le modèle et là... patatra, un contre exemple est trouvé :

Comme vous le constatez, l'utilisateur change son email avant de cliquer sur le lien et cela lui permet de valider le mauvais email. La solution devient évidente : on doit vérifier l'email auquel le lien est envoyé et non à celui de l'utilisateur.

fact { all s: Service, s': s.next | all u: s'.verified | u.(s.link) in Email - Gmail }

Et voilà que Alloy valide qu'il ne trouve plus de contre exemple, même si on augmente le nombre d'occurrence !

Alloy

C'est la première fois que j'utilise Alloy et j'ai évité de parler des problèmes que j'ai rencontré (toujours pas compris not in) et la documentation est assez peu bavarde. Par contre, il est assez simple de vérifier que le modèle est cohérent grâce à la visualisation des états. Bien que le cas choisi peut sembler assez évident, Alloy est le seul outil utilisé qui permet de valider le modèle sans lever l'ambiguïté par distinction de grammaire. Les autres outils avaient besoin de spécifier "L'email à vérifier" ou pirouette du genre pour cela, ce qui pourrait être de la triche. Il est donc normal que sa prise en main soit moins facile (j'ai pris une journée pour lire le tutoriel et réalisé le modèle tout en écrivant l'article).

Malgré ses apparences trompeuses (Alloy se donne des airs de langage orienté objet, alors que c'est vraiment un jeu sur les sets), je suis surpris d'avoir si facilement pris en main l'outil et je vais passer mon temps à imaginer comment l'utiliser au boulot. D'autant que je n'ai pas exploré l'utilisation des modules ou des fonctions.

Je suis fermement convaincu de l'utilité des outils de formalisation partielle. En apprenant à les utiliser, on apprend aussi à spécifier nos besoins avec moins d'ambiguïté. On peut plus facilement trouver la bonne représentation qui permet de faire comprendre à une personne sans connaissance sur un sujet complexe les problèmes que l'on peut rencontrer lors de son implémentation. Je ne suis néanmoins pas convaincu que les langages de formalisation comme Alloy trouveront grâce aux yeux de la majorité des développeurs vu les prérequis et la motivation nécessaire pour modéliser avec ces outils. Espérons que cet article vous aura convaincu à vous y pencher.