eventb-rossi/eventb-skill

Desarrollo de modelos Event-B

Un modelo Event-B es un sistema de transición discreto. Un CONTEXT contiene conjuntos fijos, constantes y axiomas; una MACHINE contiene variables, invariantes y eventos con guardas. Esta habilidad comprueba el comportamiento alcanzable con ProB y verifica la buena formación (well-definedness). No realiza pruebas interactivas de Rodin.

1. Verificar las herramientas necesarias

Se requiere rossi 0.1.8+ y eventb-animate 6.4+. Compruébelos; nunca los instale ni actualice usted mismo. Si alguno está ausente o es más antiguo, deténgase y pida al usuario que lo haga.

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

2. Alcance antes del modelado

Escriba una breve hoja de requisitos en el README.md del modelo:

• límites del sistema y exclusiones explícitas;
• eventos observables y quién los realiza;
• tipos de estado y las propiedades de seguridad que deben cumplirse siempre;
• un escenario de éxito alcanzable, un escenario prohibido importante y si un estado terminal es intencional.

Para un modelo sustancial o cualquier refinamiento multinivel, agregue un registro de requisito a refinamiento con una fila por nivel: cláusula de requisito/estándar, estado nuevo o reemplazado, eventos afectados, invariante/relación de pegado y pregunta de validación. Divida un nivel cuya fila contenga preocupaciones no relacionadas.

Use una máquina por defecto; divida los datos fijos en tantos contextos pequeños como sus preocupaciones independientes requieran. Agregue un nivel de refinamiento solo cuando aisle un requisito distinto o reemplace una representación de datos; escriba esa razón y el invariante de pegado primero. El refinamiento es una herramienta, no una ceremonia obligatoria.

Mantenga cada modelo en su propio directorio de proyecto. Use un componente por archivo, con el archivo nombrado según el componente. No ponga comentarios en prosa en archivos .eventb; mantenga la explicación en README.md.

3. Leer solo la referencia relevante

Necesidad	Leer
Gramática exacta de .eventb y formas de acción	references/syntax.md
Un operador o su precedencia	references/math-toolkit.md
Ayuda para elegir estado, invariantes o eventos	references/modelling.md
Un paso de refinamiento genuino, o planificar una cadena	references/refinement.md
Un patrón central de sistema reactivo	el encabezado correspondiente en references/patterns.md
Tiempo discreto, plazos, modos o sensores/actuadores	references/patterns-control.md
Múltiples participantes: topología, rondas, consenso, canales, operaciones de larga duración	references/patterns-distributed.md
Control de acceso, política de autorización o reserva	references/patterns-security.md
Derivar un bucle a partir de una postcondición, o un intérprete/ISA	references/patterns-algorithms.md
Solución de problemas de CLI o un comando avanzado condicional	references/tooling.md
Revisión final de diseño	references/best-practices.md

Comience desde examples/counter/ solo cuando estén involucrados testigos o refinamiento de datos; use examples/cars_on_bridge/ para división/convergencia de eventos y examples/array_maximum/ para algoritmos terminantes. No lea ejemplos solo para comenzar un modelo pequeño de una sola máquina.

4. Escribir el modelo útil más pequeño

• Coloque conjuntos portadores y política/configuración fija en un contexto.
• Tipifique cada variable con su primer invariante, luego indique la regla de seguridad real.
• Cuando la detección o el control cruce un límite del sistema, mantenga el estado físico, reportado y comandado distintos e indique el retraso/incertidumbre permitido entre ellos.
• Haga que INITIALISATION establezca cada invariante.
• Dé a cada evento todas las guardas requeridas por los requisitos funcionales y de solo transición, así como la preservación de invariantes; las acciones se ejecutan simultáneamente y las variables no asignadas permanecen sin cambios.
• Represente un resultado importante en el estado cuando un objetivo de estado posterior deba observarlo. No agregue un evento sin operación solo para obtener cobertura; un evento sin operación habilitado cambia el comportamiento de interbloqueo y vivacidad.
• Mantenga pequeños los escenarios de verificación finita. Los parámetros no deterministas amplios multiplican las habilitaciones de operación y pueden hacer que una verificación finita sea incompleta o lenta.

5. Ejecutar la compuerta principal

Ejecute desde el directorio del proyecto del modelo, no desde un directorio padre que contenga modelos no relacionados. Construya un .zip; contiene los archivos verificados que necesita el animador.

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

Acepte el resultado solo cuando:

• la validación y la compilación no tengan errores; trate las advertencias missing or ill-typed witness y event is inaccurate como fallos incluso si el comando sale con código cero;
• el informe tenga status: "ok" y ninguna violación de invariante;
• no haya ningún interbloqueo inesperado; para un estado terminal deliberado, documente el predicado terminal y vuelva a ejecutar con --no-deadlock en lugar de afirmar libertad de interbloqueo;
• el bloque Covered operations contenga los eventos esperados (el informe v3 no almacena la cobertura de operación, por lo que capture la salida del comando cuando esto deba auditarse);
• completion.classification sea complete para un escenario de aceptación finito;
• cada obligación de buena formación esté descargada.

Un código de salida cero no es prueba de completitud. Si un modelo finito se reporta como incompleto, inspeccione la razón y los límites relevantes de ProB:

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

Aumente MAX_INITIALISATIONS o MAX_OPERATIONS solo lo suficiente para enumerar las opciones finitas conocidas, luego vuelva a ejecutar y exija completion.classification: "complete". Para un modelo intencionalmente genérico/ilimitado, reporte el resultado acotado honestamente y agregue un escenario finito pequeño separado cuando una compuerta exhaustiva sea importante.

Si hay una cadena de refinamiento, repita la verificación del modelo y wd para cada nivel con -m <machine>.

6. Agregar evidencia dirigida cuando responda una pregunta

Use una traza de objetivo cuando la pregunta sea si un predicado de estado es alcanzable:

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 objetivo alcanzado sale deliberadamente con código 1; exija una reproducción PERFECT. Ante un fallo de invariante o interbloqueo, guarde y reproduzca su contraejemplo antes de cambiar el modelo.

Un objetivo de estado no puede probar que se disparó un evento sin acción o solo con guardas: puede detenerse tan pronto como se alcance el estado habilitador. Confirme una transición específica a través del bloque Covered operations de la verificación completa, o enfoque en ella con generación de pruebas:

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

Use estos solo cuando su propósito específico aplique:

• testgen: atestiguar una transición específica o generar accesorios de operación reproducibles; no es una compuerta más fuerte que una verificación exhaustiva, y “no cubierto” es inconcluso.
• --symbolic ic3|kinduction: seguridad de invariante no acotada; no verifica interbloqueo, reporta cobertura de eventos ni proporciona trazas.
• po: compuerta para un proyecto Rodin existente que ya tenga pruebas .bpo/.bps.
• import/export: intercambio con Rodin, no el ciclo normal de autoría.

Consulte references/tooling.md para estos flujos de trabajo condicionales. El backend predeterminado de ProB es la ruta de autoría normal.

7. Finalizar con un artefacto legible

Entregue los archivos .eventb más un README.md breve que contenga alcance, forma del modelo, el invariante de seguridad en lenguaje sencillo, cualquier registro de refinamiento, comandos exactos de verificación, completitud, cobertura de eventos, resultado de WD y cualquier abstracción deliberada. Una ejecución acotada limpia significa “no se encontró ningún error dentro del límite.” Una ejecución finita completa prueba solo el comportamiento alcanzable verificado: aún puede aceptar un invariante demasiado fuerte y no inductivo porque los estados violadores son inalcanzables. No descarga las obligaciones de prueba de invariante/refinamiento de Event-B; solo una compuerta de prueba aplicable respalda esa afirmación. Consulte references/refinement.md, “la verificación de modelos no es prueba.”