Améliorer la modélisation logicielle avec des retours en direct

Les outils de recherche de modèles finis aident les utilisateurs à décrire les caractéristiques d'un système avec des maths et ensuite à trouver automatiquement des exemples qui correspondent à ces caractéristiques. Ces exemples sont précieux car ils permettent aux développeurs de voir comment leur modèle fonctionne en pratique. Pourtant, les utilisateurs constatent souvent que les exemples ne les aident pas autant qu'ils le pensaient. Les chercheurs pensaient auparavant que c'était parce qu'il y avait trop d'exemples à examiner. Mais des études récentes montrent que les utilisateurs préfèrent en fait avoir plein d'exemples à choisir. En réalité, le souci pourrait venir du fait que les exemples sont trop éloignés des règles qui les ont créés, ce qui rend difficile la compréhension de ces règles.

#Défis dans la modélisation logicielle

Les langages de modélisation logicielle se sont beaucoup améliorés, et l'analyse de ces modèles est devenue beaucoup plus efficace. Cependant, beaucoup de gens n'utilisent pas largement les modèles logiciels. C'est principalement parce que rédiger les descriptions de ces modèles reste un gros défi. Alors que les experts peuvent rédiger ces spécifications, ils peuvent manquer de connaissances spécifiques sur les systèmes qu'ils modélisent. Idéalement, les gens qui construisent le logiciel écriraient ces spécifications.

Malheureusement, les langages de modélisation sont difficiles à apprendre, et les outils utilisés pour la modélisation sont souvent dépassés par rapport aux derniers environnements de développement. Un gros problème est le manque de retours utiles. Quand un modèle est exécuté, les utilisateurs obtiennent généralement une simple réponse oui ou non sur le fait que le modèle fonctionne ou non. Cela ne les aide pas vraiment à comprendre s'ils ont bien écrit leur modèle.

Beaucoup de fonctionnalités qui pourraient aider à l'écriture, comme les suggestions de code, manquent aussi. Pour résoudre le problème des retours, des outils de recherche de modèles finis ont été créés. Les utilisateurs écrivent un modèle de la conception de leur système, et l'outil de recherche leur fournit des exemples concrets de la façon dont le modèle se comporte. Ce résultat est appelé Solutions. Au lieu d'une simple réponse oui ou non, ces solutions fournissent plus d'informations détaillées sur le bon fonctionnement du modèle. Ces exemples peuvent aider les utilisateurs à valider leurs conceptions, tester du code, corriger des problèmes, et analyser la sécurité des systèmes.

#Préférences des utilisateurs et solutions

Bien que beaucoup voient les solutions comme le principal avantage des outils de recherche de modèles finis, les utilisateurs les trouvent souvent moins utiles que prévu. Beaucoup pensent qu'avoir trop de solutions crée de la confusion. À cause de cela, beaucoup de travail a été fait pour réduire le nombre de solutions en ajoutant plus de critères pour ce qui fait une bonne solution. Mais des découvertes récentes suggèrent que les utilisateurs préfèrent avoir plus d'exemples à explorer.

Des études utilisateurs montrent que, qu'ils soient débutants ou experts, les utilisateurs ont du mal à inspecter les solutions et à améliorer leurs modèles en fonction d'elles. Cela indique que la communauté s'attaque au mauvais problème. Il semble que les solutions soient claires mais déconnectées des règles sous-jacentes qui les créent, laissant les utilisateurs comprendre comment leurs règles abstraites influencent les exemples qu'ils voient.

L'objectif est de créer un environnement de développement où l'écriture du modèle et son évaluation se font en même temps. Cela pourrait transformer les solutions générées par les outils de recherche de modèles finis en retours utiles, rendant la modélisation logicielle plus facile pour les développeurs de logiciels ordinaires.

#Programmation en direct dans Alloy

Cette section parle d'un environnement de programmation en direct pour le langage de modélisation Alloy. Alloy permet aux utilisateurs de définir à la fois des propriétés structurelles et comportementales avec des règles logiques spécifiques. Cet environnement assistera les utilisateurs en fournissant des retours en temps réel pendant qu'ils écrivent leurs modèles.

#Motivation pour la programmation en direct

Pour démontrer l'approche de programmation en direct, imaginons comment un utilisateur définirait une structure de données de file d'attente dans Alloy. D'abord, il écrit son modèle dans l'éditeur de texte de l'outil d'analyse. Il définit des groupes d'objets, ou atomes, et comment ils se rapportent les uns aux autres. L'utilisateur crée des règles pour s'assurer que le modèle se comporte comme prévu, par exemple en s'assurant qu'aucun objet ne pointe vers lui-même et que tous les objets sont inclus dans la file d'attente.

Une fois prêt, l'utilisateur exécute une commande pour vérifier son modèle, ce qui amène le moteur d'analyse à rechercher toutes les solutions potentielles qui correspondent aux règles de l'utilisateur. Les solutions sont affichées dans une fenêtre séparée, où les utilisateurs peuvent voir les différents résultats. S'ils découvrent une solution qui ne devrait pas exister, ils peuvent modifier leur modèle dans l'éditeur de texte et répéter le processus pour voir comment leurs changements affectent les résultats.

Cependant, cette approche a ses limites. Les utilisateurs doivent penser séparément à la façon dont leurs règles vont impacter les exemples affichés. Une configuration de programmation en direct permettrait aux utilisateurs de voir ces effets en temps réel pendant qu'ils écrivent leurs règles, s'assurant qu'ils savent comment chaque changement modifie les résultats possibles.

#Suggestions pour l'amélioration

Pour améliorer l'expérience de développement dans Alloy, l'équipe a créé un prototype avec des boîtes de suggestions pour aider les utilisateurs avec leurs formules. Ces boîtes fournissent des formules recommandées et montrent comment elles fonctionneraient avec le modèle actuel. C'est similaire à la façon dont beaucoup d'environnements de programmation suggèrent des commandes valides à écrire.

En plus, les utilisateurs peuvent passer entre deux modes d'affichage : un qui affiche tous les résultats potentiels et un autre qui se concentre sur un résultat spécifique. De cette façon, les utilisateurs peuvent avoir une vision plus claire de comment leurs règles façonnent leur modèle et ses solutions.

#Vue d'énumération dynamique

La vue d'énumération dynamique montre deux ensembles de solutions à côté de l'éditeur de texte. Un ensemble consiste en solutions valides, et l'autre contient des solutions invalides. Au fur et à mesure que les utilisateurs ajoutent des règles au modèle, ils peuvent voir comment les solutions valides et invalides changent. C'est important car comprendre à la fois les solutions valides et invalides aide les utilisateurs à en apprendre davantage sur le modèle.

Dans cette vue, le programme classera les solutions en quatre groupes : solutions valides qui restent valides, nouvelles solutions valides, solutions invalides qui restent invalides, et nouvelles invalides. Cela permet aux utilisateurs de voir comment leurs changements affectent les résultats dans l'ensemble.

#Vue de focus

Bien que les utilisateurs s'intéressent à toutes les solutions, ils peuvent aussi vouloir se concentrer sur des solutions spécifiques qu'ils s'attendent à ce qu'elles fonctionnent ou non selon leurs règles. La vue de focus permet aux utilisateurs de faire exactement cela. Ils peuvent sélectionner une solution qu'ils veulent surveiller et l'étiqueter comme censée être valide ou invalide.

Pendant qu'ils écrivent, ils peuvent vérifier continuellement si la solution sélectionnée correspond à leurs attentes. Si ce n'est pas le cas, le système fournit des informations sur des solutions similaires pour aider les utilisateurs à comprendre ce qui n'a pas fonctionné.

#Directions futures

Pour passer l'environnement de programmation en direct du concept à la réalité, deux défis principaux doivent être relevés. D'abord, les prototypes pour différentes interfaces doivent être affinés pour s'assurer que les utilisateurs reçoivent des informations utiles sans être submergés. Il est essentiel de trouver la meilleure façon de présenter les informations, par exemple si les solutions doivent être similaires ou si afficher des solutions plus grandes ajoute de la clarté ou crée un désordre.

Deuxièmement, le système doit être réactif. Étant donné que le système d'analyse d'Alloy peut être lent, il est nécessaire de trouver des moyens de faire fonctionner l'environnement sans lag. Il existe des méthodes existantes qui peuvent aider à accélérer le processus d'analyse, et celles-ci devraient être utilisées pour maintenir une expérience utilisateur positive.

#Recherche connexe

La programmation en direct suscite de l'intérêt dans divers domaines de la programmation, mais son application dans les langages de modélisation a été limitée. Il existe des systèmes qui tentent de clarifier pourquoi des exemples spécifiques apparaissent dans les solutions ou qui décomposent les solutions en composants satisfaisant des règles particulières. Ces systèmes pourraient être des ajouts précieux à un environnement de programmation en direct, offrant des explications pour les solutions au fur et à mesure qu'elles sont générées.

Au final, il y a une déconnexion entre les règles d'un modèle et les solutions produites, rendant difficile pour les utilisateurs de voir à quel point ils ont bien écrit leurs modèles. Cet environnement de programmation en direct vise à combler cette lacune en intégrant l'écriture et l'évaluation des modèles, permettant aux utilisateurs de répondre à la question : "Ai-je bien écrit mon modèle ?"