Este estudio presenta un marco formal de verificación para mecanismos de consenso blockchain y contratos inteligentes, empleando el método Evento-B. Este enfoque combina la abstracción de la representación, la demostración basada en invariantes y la comprobación temporal del modelo con comprobaciones formales de seguridad, vivacidad y resistencia al doble gasto antes del despliegue.
Artículo de investigación
Verificación formal de los mecanismos de consenso blockchain usando Evento-B
En este artículo
Resumen
Resumen
Este estudio desarrolla un marco de verificación formalmente fundamentado para los mecanismos de consenso blockchain y el comportamiento de contratos inteligentes utilizando Evento-B y la plataforma Rodin. A diferencia de enfoques anteriores que se basan principalmente en la simulación o la validación basada en casos de contratos aislados, este trabajo integra abstracción de Máquina de Estados Finitos (FSM), pruebas impulsadas por invariantes, modelado de refinamiento y verificación lógica temporal para analizar la Prueba de Trabajo (PoW), la Prueba de Participación (PoS) y mecanismos para la prevención de doble gasto. Los contratos inteligentes de solidez se abstraen en FSM y se codifican como máquinas Evento-B, permitiendo la especificación formal de transiciones de estado y restricciones de seguridad. Las propiedades de seguridad —incluyendo la unicidad de la transacción, la consistencia de estado, la aplicación del control de acceso y la preservación invariante del libro mayor— se verifican mediante obligaciones de prueba generadas automáticamente en Rodin. Se generaron un total de 312 obligaciones de prueba, de las cuales 287 (92%) se cancelaron automáticamente y 25 se demostraron de forma interactiva, resultando en una cobertura completamente invariante. Las propiedades de vivacidad se especificaban en Computation Tree Logic (CTL) y se validaban mediante comprobación de modelos, confirmando la libertad de bloqueos y la eventual selección del validador bajo condiciones PoS. La prevención del doble gasto se aplicó formalmente mediante modelado de libro mayor consistente en el estado, donde se demostraron las restricciones de unicidad en todos los estados accesibles. La lógica de consenso a nivel de protocolo para PoW y PoS se perfeccionó en tres niveles de abstracción, asegurando la integridad del bloque y la corrección del validador mediante un refinamiento paso a paso. Los resultados demuestran que las pruebas verificadas por máquina ofrecen garantías de corrección verificables más allá de la evaluación basada en simulación, estableciendo una cadena de verificación rigurosa y reproducible que mejora la garantía de la corrección y la robustez a nivel de protocolo en los sistemas blockchain.
Introducción
La tecnología blockchain ha evolucionado hacia un paradigma de libro mayor distribuido que permite el registro descentralizado sin depender de autoridades centralizadas. Al replicar los estados del libro mayor entre los nodos participantes y lograr acuerdos mediante mecanismos de consenso, los sistemas blockchain proporcionan integridad, transparencia y resistencia a la manipulación en entornos abiertos y adversariales. Como describen Yaga et al.1, la arquitectura blockchain combina primitivas criptográficas, protocolos de consenso distribuidos y comunicación peer-to-peer para garantizar que las transacciones validadas se vuelvan computacionalmente impracticables de modificar. Mecanismos de consenso fundamentales como la Prueba de Trabajo (PoW) y la Prueba de Stake (PoS) regulan la selección del validador, la validación de bloques y la sincronización del libro mayor. Además, los contratos inteligentes amplían las capacidades de blockchain al integrar lógica programable que ejecuta de forma autónoma reglas predefinidas, permitiendo aplicaciones descentralizadas en sectores como finanzas, sanidad y gobernanza. A medida que las tecnologías blockchain se despliegan cada vez más en entornos de alto valor y críticos para la seguridad, garantizar la corrección de los mecanismos de consenso y el comportamiento de los contratos inteligentes se ha vuelto esencial para mantener la fiabilidadoperativa 2.
A pesar de su naturaleza descentralizada, los sistemas blockchain siguen siendo susceptibles a vulnerabilidades lógicas y a nivel de protocolo. Los ataques de doble gasto pueden ocurrir cuando las restricciones de consistencia del libro mayor no se aplican rigurosamente. Debilidades a nivel de consenso, como una lógica incorrecta de selección de validadores o reglas de validación de bloques defectuosas, así como vulnerabilidades en contratos inteligentes, como la reentrada y un control de acceso inadecuado, han provocado pérdidas financieras sustanciales en plataformas desplegadas. Aunque los marcos de pruebas empíricas y simulación se utilizan ampliamente para evaluar el comportamiento de los protocolos PoW y PoS, estos enfoques solo proporcionan observaciones ilustrativas en lugar de garantías de corrección exhaustivas. La validación basada en simulación no puede demostrar la preservación invariante en todos los estados alcanzables ni garantizar propiedades de seguridad y vivacidad en cada ruta de ejecución. Esta limitación pone de manifiesto la necesidad de técnicas de verificación fundamentadas en matemáticas que puedan razonar rigurosamente sobre los sistemas blockchain más allá del análisis observacional.
Los métodos formales ofrecen esta base al permitir la especificación y verificación del sistema mediante lógicamatemática 3,4. El evento-B amplía este paradigma mediante el refinamiento paso a paso, representando los sistemas como máquinas de estados abstractas en las que los estados del sistema están restringidos por invariantes y las transiciones se modelan como eventosprotegidos 5. La plataforma Rodin genera automáticamente obligaciones de prueba y soporta su descarga, permitiendo la verificación verificada por máquina de preservación invariante y la consistenciade estado 6. Técnicas clásicas de especificación como el B-Método7 y Z8 demuestran cómo el razonamiento basado en invariantes y el refinamiento formal pueden garantizar la corrección del sistema a través de diferentes etapas de desarrollo. Estos métodos se han aplicado ampliamente en sistemas críticos para la misión y seguridad para garantizar la corrección antes deldespliegue 9, 10, 11, 12 y 13. Extensiones adicionales como UML-B y marcos de refinamiento gráfico demuestran aún más la escalabilidad del modelado basado en refinamiento para sistemas industrialescomplejos 14,15,16,17,18,19. Estos desarrollos ilustran que el modelado formal basado en el refinamiento puede gestionar eficazmente la complejidad del sistema manteniendo garantías sólidas de corrección.
También se han explorado enfoques formales de verificación para sistemas blockchain. Las técnicas de verificación de contratos basadas en SMT verifican automáticamente las afirmaciones dentro de los programas Solidity y pueden producir contraejemplos cuando ocurren violacioneslógicas 20. Herramientas como VERISOL emplean abstracciones de estado finito para la verificación de contratosinteligentes 2, mientras que los enfoques de demostración de teoremas traducen contratos en marcos de razonamiento formal como F*21. Además, las formalizaciones semánticas de la Máquina Virtual de Ethereum permiten un razonamiento riguroso sobre la semántica de ejecución y la detecciónde vulnerabilidades 22. De manera similar, se han aplicado entornos de demostración de teoremas como Coq para analizar propiedades de seguridad relacionadas con el consenso y la correccióntransaccional 23. Aunque estos enfoques aportan valiosas perspectivas, a menudo se centran de forma independiente en la corrección a nivel de contrato o en las propiedades a nivel de consenso. Los invariantes del libro mayor a nivel de sistema, las transiciones de estado de consenso y el comportamiento de contratos inteligentes rara vez se integran dentro de un marco unificado basado en refinamiento que mantenga la trazabilidad entre capas de especificación y artefactos de verificación. Además, muchos enfoques existentes enfatizan la detección de vulnerabilidades o la comprobación lógica de aserciones en lugar de la preservación sistemática de invariantes a través de múltiples niveles de refinamiento.
El presente estudio aborda esta carencia metodológica proponiendo un marco unificado de verificación formal que integra la abstracción de contratos inteligentes Solidity con la Máquina de Estados Finitos (FSM) con modelado de refinamiento Evento-B y descarga de obligaciones de prueba comprobadas por máquina dentro de la plataforma Rodin. En lugar de tratar la verificación de contratos y el modelado por consenso como problemas separados, el marco propuesto especifica formalmente las transiciones de estado a nivel de protocolo para PoW y PoS, restricciones de integridad del libro mayor, condiciones de unicidad de transacciones y evolución del estado de contratos inteligentes dentro de un único modelo estructurado. Las propiedades de seguridad —incluyendo la preservación invariante, la unicidad de la transacción, las transiciones de estado controladas y la consistencia del libro mayor— se expresan como invariantes del Evento-B y se verifican mediante obligaciones de prueba generadas automáticamente. Las propiedades temporales y dependientes del orden de ejecución se especifican usando la Lógica del Árbol de Computación y se verifican mediante comprobación de modelos para asegurar la corrección más allá de los invariantes estáticos. Una contribución metodológica clave radica en establecer una trazabilidad explícita a través de capas de abstracción: las funciones de solidez se abstraen en transiciones FSM, las transiciones FSM se codifican como eventos Evento-B, y los invariantes junto con especificaciones temporales se vinculan directamente a obligaciones de prueba liberadas y a resultados de verificación de modelos. Este mapeo estructurado garantiza que cada afirmación de corrección esté respaldada por evidencia verificada por máquina y distinga claramente las garantías basadas en pruebas de las observaciones basadas en simulación.
El alcance de este trabajo está deliberadamente restringido para garantizar precisión y claridad analítica. El modelado se centra en las transiciones de estado a nivel de protocolo para mecanismos de consenso, restricciones de integridad del libro mayor, propiedades de unicidad de transacciones y comportamiento del estado de los contratos inteligentes. Aspectos a nivel de red, como los retrasos en la propagación de mensajes, estrategias adversariales bizantinas, mecanismos de resolución de forks y semántica detallada de gas de la máquina virtual de Ethereum, quedan fuera del límite de abstracción definido. Al definir explícitamente estas suposiciones de modelización, el marco garantiza que las afirmaciones de verificación permanezcan alineadas con la evidencia de prueba formalmente verificada. El resto de este artículo presenta la metodología de abstracción, el proceso de modelado y refinamiento Evento-B, los procedimientos para la verificación invariante y temporal, y los resultados resultantes de la verificación. Al fundamentar el protocolo blockchain y la verificación de contratos inteligentes en modelado formal basado en refinamiento y pruebas verificadas por máquina, este estudio refuerza el rigor metodológico y mejora la garantía de corrección previa al despliegue para sistemas de libro mayor descentralizados.
Acceso restringido. Inicie sesión o comience una prueba gratuita para ver este contenido.
Protocolo
Aportaciones de estudio
En este estudio, se utilizaron dos contratos inteligentes Solidity como entradas de verificación. El primero fue un contrato al estilo Simple DAO que se utilizó como caso de estudio de reentrada. El segundo era un contrato de libro mayor/transición de estado simplificado diseñado para probar las restricciones a nivel de contrato frente al doble gasto. El código fuente original de Solidity servía como entrada a los procesos de abstracción y verificación definidos en este protocolo. El proceso general de transformación utilizado para dichos contratos se ilustra en la Figura 1, que muestra la transformación gradual del código fuente de Solidity en los modelos FSM, Evento-B y SMV durante la verificación.
Modelado de frontera
El modelado formal se centra en la lógica de control y flujo de los contratos inteligentes, incluyendo el comportamiento de entrada y salida de funciones, la ejecución interna y las transiciones de estado a nivel de contrato. La visibilidad de funciones (pública, externa, interna y privada) se representó junto con el comportamiento correspondiente de la pila de llamadas relevante para el análisis de reentrancia. Los tipos de transiciones abstractas (llamada, envío, transferencia) se trataban como operaciones para transferir éteres.
Se definieron invariantes a nivel de contrato para asegurar la unicidad de la transacción y evitar el doble gasto dentro del límite de abstracción. Para representar los requisitos de selección de validación e integridad del bloque, la capa de abstracción lógica-protocolo se definió en términos de las transiciones de estado a nivel de protocolo tanto de Proof of Work como de Proof of Stake.
El límite de abstracción no incluía elementos de la capa de red, incluyendo la programación de los mensajes a entregar y los retrasos causados por cualquier número de saltos, resolución de forks, adversarios de la red empleando estrategias bizantinas, semántica de la Máquina Virtual de Ethereum y semántica de gas controlada por nodos de red, propagación de excepciones, ejecuciones asíncronas, comportamientos de retroceso complejos y finalización a nivel de red. Por tanto, los resultados de la determinación del doble gasto solo se aplican a invariantes a nivel de contrato y no constituyen un acuerdo a nivel de red sobre la finalidad.
Herramientas y configuración
La plataforma Rodin se utilizó para modelar, refinar, generar obligaciones de prueba y ejecutar el modelo Evento-B (versión 3.7.0), que permitía que los probadores PP, ML, SMT y Atelier-B descargaran pruebas de forma automática e interactiva. la versión 2.0.0 de nuXmv se ejecutó en los modelos SMV generados en modo de exploración CTL completa para realizar comprobaciones de modelos CTL.
Todas las ejecuciones de verificación se realizaron en un entorno computacional controlado usando Ubuntu 22.04 LTS, OpenJDK 11 y Python 3.10.12. Web3 (7.6.0), NetworkX (3.4.2), Matplotlib (3.8.0), Graphviz (0.20.3), NumPy (1.26.4) y Pandas (2.2.2) se utilizaron para implementar elementos de simulación y visualización. Este diseño garantizaba que los resultados formales de verificación y simulación pudieran reproducirse cuando se ejecutaban bajo las mismas condiciones de ejecución.
Flujo de trabajo de transformación
Este proceso de verificación constaba de cuatro fases. Los contratos de solidez se tradujeron primero en una representación de Máquina de Estados Finitos (FSM-SC). El modelo FSM-SC fue posteriormente codificado en Evento-B, con invariantes y grados de refinamiento claramente especificados. La abstracción FSM-SC se tradujo en un modelo SMV en nuXmv. Los resultados de la verificación se informaron como estadísticas sobre la cancelación de obligaciones de prueba y la verificación por modelo CTL, y se proporcionaron contraejemplos como casos.
Construcción de FSM
Cada contrato se abstrajo como una Máquina de Estados Finitos definida como:
Donde:
S = conjunto de estados
S₀ = estado inicial
T = relación de transición
V = mapeo de visibilidad
G = predicados de guardia
A = acciones/actualizaciones de estado.
Algoritmo 1: Construcción FSM a partir de Solidity
Entrada: Código fuente de Solidity
Salida: FSM-SC
1) Analizar el árbol sintáctico abstracto del contrato de Solidity.
2) Crear el estado inicial S₀ a partir de la definición del constructor.
3) Para cada función de solidez f, crear un estado de control distinto S_f y registrar visibilidad V(f) ∈ {público, externo, interno, privado}.
4) Para cada sentencia dentro de la función f, se deriva una transición t extrayendo predicados de guardia de condiciones de requerimiento/afirmación y acciones de actualizaciones de variables de estado.
5) Añadir la transición t a T.
6) Crear tipos de transición explícitos para operaciones de transferencia Ether (llamada, envío, transferencia), llamadas internas y externas, llamada delegada, autodestrucción, uso de tx.origin, ramas condicionales y construcciones de bucle.
7) Retorno FSM-SC = (S, S₀, T, V, G, A).
Y cada función de solidez está asociada a un estado de control FSM diferente. Para la comprensión de vulnerabilidades, los flujos de ejecución relevantes para vulnerabilidades, por ejemplo, tales flujos con llamadas externas seguidas de actualizaciones de balance, se abstrajeron explícitamente en transiciones ordenadas. La Figura 2 describe un diagrama de ejemplo FSM-SC para el contrato al estilo SimpleDAO, mostrando cómo se abstrajeron los estados de entrada, las transiciones de llamadas externas y las secuencias de actualización de estado durante esta etapa de construcción.
Codificación de FSM en Evento-B
La transición FSM se representó como constructos Evento-B. Todas las transiciones corresponden a eventos del Evento-B, incluyendo guardias y acciones particulares.
Algoritmo 2: Codificación FSM a Evento-B
Entrada: FSM-SC
Salida: Máquina de evento B y contexto
1) Definir STATE_SET y FUNCIÓN en el contexto contractual.
2) Declarar variables que representen el estado de control FSM y el estado a nivel de contrato.
3) Representar cada estado de control FSM s ∈ S usando current_state ∈ STATE_SET.
4) Para cada transición (s → s′, g, a), crear un evento Evento-B E_t con:
5) DONDE current_state = s ∧ g
6) ENTONCES current_state := s′ ∥ aplicar(a)
7) Codificar restricciones de visibilidad usando guardas derivadas de V(f).
8) Definir invariantes inv1–inv9 para capturar propiedades de seguridad y consistencia.
9) Definir la INICIALIZACIÓN asignando valores S₀ y por defecto.
El conjunto de estados, el estado actual, la visibilidad de la función, la pila de llamadas, la marca de tiempo de la transacción, el estado de transferencia de Ether, la bandera de llamada de delegado, la bandera de autodestrucción y la condición de verificación son algunas de las variables que se capturan en el modelo Evento-B. Los invariantes (inv1-inv9) y las acciones de las inicializaciones (acto1-acto6) coinciden con las de la especificación formal. La Figura 3 también ofrece una representación gráfica de cómo se mantienen los eventos clave relevantes para vulnerabilidades, especialmente las transiciones relacionadas con la reentrancia, en la codificación Evento-B. Esta figura explica cómo los patrones estructurales del modelo FSM-SC mostrado en la Figura 2 se mapean en eventos verificables de Evento-B.
Estrategia de refinamiento
Se implementaron dos niveles de refinamiento. Los invariantes de control de control de alto nivel del contrato y núcleos se representaban a nivel abstracto. El nivel refinado añadió restricciones específicas del contrato, incluyendo restricciones de pila de llamadas, restricciones de visibilidad y condiciones de prevención de reentrada.
Algoritmo 3: Refinamiento y exoneración de la prueba y la obligación
Entrada: Máquina abstracta y máquina refinada
Resultados: Obligaciones de prueba y estadísticas exhaladas
1) Generar obligaciones de demostración para la máquina abstracta en Rodin.
2) Ejecutar probadores automáticos habilitados y registrar los resultados de descarga.
3) Generar obligaciones de prueba de refinamiento para la máquina refinada.
4) Aplicar evaluadores automáticos a las obligaciones de refinamiento.
5) Cumplir con las obligaciones restantes de forma interactiva cuando sea necesario.
6) Estadísticas de pruebas de exportación e informes de estado.
La presentación de pruebas incluyó el número de invariantes, los niveles de refinamiento, las obligaciones de prueba generadas, la tasa de descarga automática, la tasa de descarga interactiva y la tasa final de descarga.
Especificación de propiedades CTL y verificación de modelos
La abstracción FSM-SC se tradujo en un modelo SMV para la verificación temporal en tiempo de ramificación en nuXmv.
Algoritmo 4: FSM a SMV y comprobación CTL
Salida: resultado de verificación PASS/FAIL y trazas de contraejemplo (si las hay)
1. Registrar los estados de control FSM como un estado enumerado de variables SMV.
2. Convertir transiciones FSM en asignaciones de siguiente estado protegidas.
3. Mantener alertas para condiciones relevantes para vulnerabilidades, como llamadas externas y actualizaciones de balance.
4. Codificar propiedades CTL en nuXmv y realizar comprobaciones de modelos.
5. Si una propiedad falla, genera trazas de contraejemplo que representen secuencias de transición FSM.
La comprobación CTL incluía requisitos de órdenes de reentrada, finalización de actualizaciones de estado tras operaciones de transferencia, limitación de la entrada recursiva sin restricciones en secciones críticas y evitación de bloqueos.
Propiedades de seguridad verificadas
El contrato tipo DAO simple que evita la reentrada se confirmó asegurando un orden seguro entre llamadas externas y actualizaciones de estado mediante invariantes y restricciones CTL. Cuando se permitía, estos guardias comprobaban las restricciones de control de acceso, asegurándose de que las transiciones no autorizadas estuvieran restringidas por invariantes. El modelo del libro mayor reducido verificó los invariantes de la unicidad de las transacciones y la consistencia del libro mayor a nivel de prevención dentro del contrato.
Resultados reportados
La sección de Resultados proporciona informes sobre métricas estructurales de FSM, métricas del modelo Evento-B y estadísticas para la verificación de prueba de obligación y CTL. Los resultados de la prueba formal y los de la verificación de modelos CTL se presentan por separado para distinguir la evidencia de garantías de corrección por invariantes y la evidencia de una verificación temporal mediante verificación temporal.
Acceso restringido. Inicie sesión o comience una prueba gratuita para ver este contenido.
Resultados
Los hallazgos de este trabajo combinan los productos formales de verificación de modelos Evento-B y CTL con información ejecutable de la simulación blockchain. La combinación de estos resultados multicapa permite validar comportamientos clave en contratos inteligentes, sus sistemas de consenso y sus limitaciones de validez en el libro mayor dentro de la limitada ejemplificación del diseño.
Configuración del entorno y verificación de dependencias
Acceso restringido. Inicie sesión o comience una prueba gratuita para ver este contenido.
Discusión
La verificación formal y basada en simulación demuestra que el sistema de verificación multilayer utilizado en la investigación era capaz de verificar el comportamiento de los contratos inteligentes, la corrección del mecanismo de consenso y la propiedad de integridad del libro mayor bajo el límite de abstracción bien definido. El evento-B proporciona una representación matemáticamente fundamentada de las propiedades de seguridad, una lógica de flujo de estados y lógica de prevención de ...
Acceso restringido. Inicie sesión o comience una prueba gratuita para ver este contenido.
Divulgaciones
Los autores no tienen conflictos de interés que declarar.
Materiales
| Nombre | Empresa | Número de catálogo | Comentarios |
|---|---|---|---|
| Rodin Platform (v3.7.0) | Rodin Team / Fundación Eclipse | https://www.event-b.org/install.html | Modelado de evento-B, refinamiento y generación y descarga de obligaciones de prueba |
| Método Evento-B | Universidad de Southampton / Comunidad Rodin | https://www.event-b.org/ | Marco de modelado formal para la especificación y refinamiento de invariantes |
| Comprobador de modelos nuXmv (v2.0.0) | FBK (Fondazione Bruno Kessler) | https://nuxmv.fbk.eu/ | Comprobación simbólica de modelos de propiedades CTL |
| Graphviz (v0.20.3) | Equipo de Graphviz | https://graphviz.org/ | Visualización FSM y renderizado de gráficos |
| Python (v3.10.12) | Fundación de Software Python | https://www.python.org/downloads | Entorno de simulación y ejecución |
| Web3.py (v7.6.0) | Fundación Ethereum / Colaboradores | https://web3py.readthedocs.io/ | Interacción blockchain y simulación de transacciones |
| NetworkX (v3.4.2) | Desarrolladores de NetworkX | https://networkx.org/ | Modelado de grafos de estructuras blockchain y FSM |
| Matplotlib (v3.8.0) | Equipo de Desarrollo de Matplotlib | https://matplotlib.org/ | Graficando el tiempo de minería y las distribuciones de validadores |
| NumPy (v1.26.4) | Desarrolladores NumPy | https://numpy.org/ | Cálculos numéricos |
| Pandas (v2.2.2) | Equipo de Desarrollo Pandas | https://pandas.pydata.org/ | Análisis y procesamiento de datos |
| OpenJDK 11 | Oracle / Comunidad OpenJDK | https://openjdk.org/projects/jdk/11/ | Duración requerida para la plataforma Rodin |
| Ubuntu 22.04 LTS | Canonical Ltd. | https://ubuntu.com/download | Sistema operativo para todos los experimentos |
| Solidez | Fundación Ethereum | https://soliditylang.org/ | Lenguaje fuente de contratos inteligentes utilizado como entrada |
| Lenguaje de Entrada nuXmv (SMV) | FBK | https://nuxmv.fbk.eu/documentation.html | Representación intermedia del modelo para la verificación CTL |
Referencias
- Yaga, D., Mell, P., Roby, N., Scarfone, K. Blockchain Technology Overview. , National Institute of Standards and Technology. Gaithersburg, MD, USA. (2018).
- Wang, Y., et al. Formal specification and verification of smart contracts for Azure Blockchain. arXiv preprint. , (2019).
- Huth, M., Ryan, M. Logic in Computer Science: Modelling and Reasoning About Systems. , Cambridge University Press. Cambridge, U.K. (2004).
- Baier, C., Katoen, J. P. Principles of Model Checking. , MIT Press. Cambridge, MA, USA. (2008).
- Abrial, J. R. Modeling in Event-B: System and Software Engineering. , Cambridge University Press. Cambridge, U.K. (2010).
- Abrial, J. R., et al. Rodin: An open toolset for modelling and reasoning in Event-B. Int. J. Softw. Tools Technol. Transf. 12 (6), 447-466 (2010).
- Abrial, J. R. The B-Book: Assigning Programs to Meanings. , Cambridge University Press. Cambridge, U.K. (1996).
- Jacky, J. The Way of Z: Practical Programming with Formal Methods. , Cambridge University Press. Cambridge, U.K. (1996).
- Verma, S., Yadav, D., Chandra, G. Introduction of formal methods in blockchain consensus mechanism and its associated protocols. IEEE Access. 10, 66611-66621 (2022).
- Guha, S., Nag, A., Karmakar, R. Formal verification of safety-critical systems: A case study in airbag system design. Proc. Int. Conf. Intelligent Systems Design and Applications, , Springer. Cham, Switzerland. 107-116 (2021).
- Karmakar, R. Formal verification techniques: A comparative analysis for critical system design. Proc. Int. Conf. Intelligent Systems Design and Applications, , Springer. Cham, Switzerland. 93-102 (2022).
- Karmakar, R. Symbolic model checking: A comprehensive review for critical system design. Adv. Data Inf. Sci. , Springer. Singapore. 693-703 (2022).
- Said, M. Y., Butler, M., Snook, C. A method of refinement in UML-B. Softw. Syst. Model. 14 (4), 1557-1580 (2015).
- Snook, C. F., Butler, M. J. UML-B: A plug-in for the Event-B tool set. Proc. ABZ 2008: Abstract State Machines, B and Z, , Springer. 344-358 (2008).
- Ben Younes, A., Ben Ayed, L. From UML activity diagrams to Event-B for the specification and the verification of workflow applications. Proc. IEEE 32nd Int. Conf. Computer Software and Applications, , 643-648 (2008).
- Morris, K. V., Snook, C. Reconciling SCXML Statechart Representations and Event-B Lower Level Semantics. , Sandia National Laboratories. Livermore, CA, USA. (2016).
- Butler, M. Decomposition structures for Event-B. Proc. Integrated Formal Methods (IFM 2009), , Springer. Berlin, Heidelberg. 20-38 (2009).
- Butler, M. Incremental design of distributed systems with Event-B. Proc. Integrated Formal Methods (IFM 2009), , Springer. Berlin, Heidelberg. (2009).
- Le, T. C., Garriga, M., Pautasso, C., Stankovic, M. Proving conditional termination for smart contracts. Proc. ACM Workshop Blockchains, Cryptocurrencies, and Contracts, , (2018).
- Alt, L., et al. SMT-based verification of Solidity smart contracts. Proc. ISoLA 2018: Leveraging Applications of Formal Methods, , Springer. Cham, Switzerland. 376-388 (2018).
- Bhargavan, K., et al. Formal verification of smart contracts. Proc. ACM Workshop Programming Languages and Analysis for Security, , 91-96 (2016).
- Grishchenko, I., Maffei, M., Schneidewind, C. A semantic framework for the security analysis of Ethereum smart contracts. Formal Methods Secure Software Systems (PoST 2018), , Springer. Cham. 243-269 (2018).
- Nielsen, J. B., et al. Smart contract interactions in Coq. arXiv preprint. , (2019).
Acceso restringido. Inicie sesión o comience una prueba gratuita para ver este contenido.
Reimpresiones y permisos
Solicitar permiso para reutilizar el texto o las figuras de este artículo de JoVE
Solicitar permiso