eventb-rossi/eventb-skill

Développement de modèles Event-B

Un modèle Event-B est un système de transition discret. Un CONTEXT contient des ensembles fixes, des constantes et des axiomes ; une MACHINE contient des variables, des invariants et des événements gardés. Cette compétence vérifie le comportement accessible avec ProB et les obligations de bonne définition. Elle ne rédige pas de preuves Rodin interactives.

1. Vérifier les outils requis

Nécessite rossi 0.1.8+ et eventb-animate 6.4+. Vérifiez-les ; ne les installez ni ne les mettez à niveau vous-même. Si l'un d'eux est absent ou plus ancien, arrêtez-vous et demandez à l'utilisateur de le faire.

command -v rossi eventb-animate
rossi --version
eventb-animate --version

2. Périmètre avant la modélisation

Rédigez une courte fiche d'exigences dans le README.md du modèle :

• périmètre du système et exclusions explicites ;
• événements observables et qui les exécute ;
• types d'état et propriétés de sûreté qui doivent toujours être vérifiées ;
• un scénario de succès accessible, un scénario interdit important, et si un état terminal est intentionnel.

Pour un modèle substantiel ou tout raffinement multi-niveaux, ajoutez un registre exigence-rafinement avec une ligne par niveau : clause d'exigence/norme, état nouveau ou remplacé, événements affectés, invariant/relation de collage et question de validation. Séparez un niveau dont la ligne contient des préoccupations sans rapport.

Utilisez une machine par défaut ; répartissez les données fixes dans autant de petits contextes que ses préoccupations indépendantes l'exigent. N'ajoutez un niveau de raffinement que s'il isole une exigence distincte ou remplace une représentation de données ; écrivez d'abord cette raison et l'invariant de collage. Le raffinement est un outil, pas une cérémonie obligatoire.

Conservez chaque modèle dans son propre répertoire de projet. Utilisez un composant par fichier, le fichier étant nommé d'après le composant. Ne mettez pas de commentaires en prose dans les fichiers .eventb ; conservez l'explication dans README.md.

3. Lire uniquement la référence pertinente

Besoin	Lire
Grammaire .eventb exacte et formes d'action	references/syntax.md
Un opérateur ou sa priorité	references/math-toolkit.md
Aide pour choisir l'état, les invariants ou les événements	references/modelling.md
Une étape de raffinement authentique, ou la planification d'une chaîne	references/refinement.md
Un motif de base de système réactif	l'en-tête correspondant dans references/patterns.md
Temps discret, délais, modes, ou capteurs/actionneurs	references/patterns-control.md
Participants multiples : topologie, tours, consensus, canaux, opérations longues	references/patterns-distributed.md
Contrôle d'accès, politique d'autorisation ou réservation	references/patterns-security.md
Dérivation d'une boucle à partir d'une postcondition, ou d'un interpréteur/ISA	references/patterns-algorithms.md
Dépannage CLI ou commande avancée conditionnelle	references/tooling.md
Revue de conception finale	references/best-practices.md

Commencez par examples/counter/ uniquement lorsque des témoins ou un raffinement de données sont impliqués ; utilisez examples/cars_on_bridge/ pour la séparation/convergence d'événements et examples/array_maximum/ pour les algorithmes terminaux. Ne lisez pas d'exemples simplement pour commencer un petit modèle à machine unique.

4. Rédiger le plus petit modèle utile

• Mettez les ensembles porteurs et la politique/configuration fixe dans un contexte.
• Tapez chaque variable avec son premier invariant, puis énoncez la règle de sûreté réelle.
• Lorsque la détection ou le contrôle franchit une frontière système, conservez l'état physique, rapporté et commandé distincts et énoncez le délai/incertitude autorisé entre eux.
• Faites en sorte que INITIALISATION établisse chaque invariant.
• Donnez à chaque événement toutes les gardes requises par les exigences fonctionnelles et de transition ainsi que par la préservation de l'invariant ; les actions s'exécutent simultanément et les variables non assignées restent inchangées.
• Représentez un résultat important dans l'état lorsqu'un objectif d'état ultérieur doit l'observer. N'ajoutez pas un événement sans effet uniquement pour obtenir une couverture ; un événement sans effet activé modifie le comportement de blocage et de vivacité.
• Gardez les scénarios de vérification finis petits. Des paramètres non déterministes larges multiplient les activations d'opérations et peuvent rendre une vérification par ailleurs finie incomplète ou lente.

5. Exécuter la porte centrale

Exécutez depuis le répertoire du projet du modèle, pas depuis un parent contenant des modèles non liés. Construisez un .zip ; il contient les fichiers vérifiés dont l'animateur a besoin.

rossi fmt -i .
rossi validate .
rossi fmt --check .
rossi build . -o /tmp/model.zip
eventb-animate --json /tmp/model-report.json /tmp/model.zip
eventb-animate wd /tmp/model.zip

Acceptez le résultat uniquement lorsque :

• la validation et la construction n'ont aucune erreur ; traitez les avertissements missing or ill-typed witness et event is inaccurate comme des échecs même si la commande se termine avec zéro ;
• le rapport a status: "ok" et aucune violation d'invariant ;
• il n'y a aucun blocage inattendu ; pour un état terminal délibéré, documentez le prédicat terminal et réexécutez avec --no-deadlock au lieu de prétendre à l'absence de blocage ;
• le bloc Covered operations humain contient les événements attendus (le rapport v3 ne stocke pas la couverture des opérations, donc capturez la sortie de la commande lorsque cela doit être audité) ;
• completion.classification est complete pour un scénario d'acceptation fini ;
• chaque obligation de bonne définition est acquittée.

Un code de sortie zéro n'est pas une preuve d'exhaustivité. Si un modèle fini est rapporté comme incomplet, inspectez la raison et les limites ProB pertinentes :

eventb-animate info --prefs /tmp/model.zip \
  | rg 'MAX_(INITIALISATIONS|OPERATIONS)|DEFAULT_SETSIZE'

Augmentez MAX_INITIALISATIONS ou MAX_OPERATIONS juste assez pour énumérer les choix finis connus, puis réexécutez et exigez completion.classification: "complete". Pour un modèle intentionnellement générique/non borné, rapportez honnêtement le résultat borné et ajoutez un petit scénario fini séparé lorsqu'une porte exhaustive est importante.

S'il y a une chaîne de raffinement, répétez la vérification du modèle et wd pour chaque niveau avec -m <machine>.

6. Ajouter des preuves ciblées lorsqu'elles répondent à une question

Utilisez une trace d'objectif lorsque la question est de savoir si un prédicat d'état est accessible :

eventb-animate -m M --goal '<predicate>' --no-invariant --no-deadlock \
  --save /tmp/scenario.json /tmp/model.zip
eventb-animate replay -m M -t /tmp/scenario.json /tmp/model.zip

Un objectif atteint se termine délibérément par 1 ; exigez une relecture PERFECT. En cas d'échec d'invariant ou de blocage, sauvegardez et rejouez son contre-exemple avant de modifier le modèle.

Un objectif d'état ne peut pas prouver qu'un événement sans action ou uniquement avec garde s'est déclenché : il peut s'arrêter dès que l'état d'activation est atteint. Confirmez une transition spécifique via le bloc Covered operations de la vérification complète, ou ciblez-la avec la génération de tests :

eventb-animate testgen -m M --operations EVENT_NAME \
  --out /tmp/scenario-traces /tmp/model.zip

N'utilisez ceux-ci que lorsque leur objectif plus restreint s'applique :

• testgen : témoigner une transition spécifique ou générer des fixtures d'opération rejouables ; ce n'est pas une porte plus forte qu'une vérification exhaustive, et « non couvert » est non concluant.
• --symbolic ic3|kinduction : sûreté d'invariant non borné ; il ne vérifie pas le blocage, ne signale pas la couverture des événements et ne fournit pas de traces.
• po : valider un projet Rodin existant qui contient déjà des preuves .bpo/.bps.
• import/export : échange Rodin, pas la boucle de développement normale.

Voir references/tooling.md pour ces workflows conditionnels. Le backend ProB par défaut est le chemin de développement normal.

7. Terminer avec un artefact lisible

Livrez les fichiers .eventb plus un court README.md contenant le périmètre, la forme du modèle, l'invariant de sûreté en langage simple, tout registre de raffinement, les commandes de vérification exactes, l'exhaustivité, la couverture des événements, le résultat WD et toute abstraction délibérée. Une exécution bornée propre signifie « aucun bogue trouvé dans la limite. » Une exécution finie complète prouve uniquement le comportement accessible vérifié : elle peut encore accepter un invariant trop fort et non inductif parce que les états violants sont inaccessibles. Elle n'acquitte pas les obligations de preuve d'invariant/raffinement Event-B ; seule une porte de preuve applicable soutient cette affirmation. Voir references/refinement.md, « la vérification de modèle n'est pas une preuve. »