Artigo de investigação

Verificação formal dos mecanismos de consenso blockchain usando o Evento-B

DOI:

10.3791/70193

⸱

8 de maio de 2026

 ,  , 
1Department of Computer Science & Engineering, Pranveer Singh Institute of Technology, AKTU, 2Department of Computer Science & Engineering, Institute of Engineering & Technology

Neste artigo

Resumo

$$\rightleftharpoonup{xx}$$ $$\longleftharp{xx}$$, $$\longrightharp{xx}$$,

Este estudo apresenta uma estrutura formal de verificação para mecanismos de consenso blockchain e contratos inteligentes, empregando o método Evento-B. Essa abordagem combina abstração da representação, provas baseadas em invariantes e verificação temporal do modelo com verificações formais de segurança, vivacidade e resistência ao duplo gasto antes da implantação.

Resumo

$$\rightleftharpoonup{xx}$$ $$\longleftharp{xx}$$, $$\longrightharp{xx}$$,

Este estudo desenvolve uma estrutura de verificação formalmente fundamentada para mecanismos de consenso blockchain e comportamento de contratos inteligentes usando o Evento-B e a plataforma Rodin. Diferentemente de abordagens anteriores que dependiam principalmente de simulação ou validação baseada em casos de contratos isolados, este trabalho integra abstração de Máquina de Estados Finitos (FSM), provas conduzidas por invariantes, modelagem de refinamento e verificação lógica temporal para analisar Prova de Trabalho (PoW), Prova de Stake (PoS) e mecanismos de prevenção de gastos duplos. Contratos inteligentes Solidity são abstratos em FSMs e codificados como máquinas Evento-B, permitindo a especificação formal de transições de estado e restrições de segurança. Propriedades de segurança — incluindo unicidade de transação, consistência de estado, fiscalização do controle de acesso e preservação invariante do livro razão — são verificadas por meio de obrigações de prova geradas automaticamente no Rodin. Um total de 312 obrigações de prova foram geradas, das quais 287 (92%) foram quitadas automaticamente e 25 foram comprovadas interativamente, resultando em cobertura completamente invariante. As propriedades de vivacidade foram especificadas na Computation Tree Logic (CTL) e validadas por meio de verificação de modelos, confirmando a liberdade de deadlock e a eventual seleção do validador sob condições PoS. A prevenção de gastos duplos foi formalmente aplicada usando modelagem de razão consistente com estado, onde as restrições de unicidade foram comprovadas em todos os estados alcançáveis. A lógica de consenso em nível de protocolo para PoW e PoS foi refinada em três níveis de abstração, garantindo integridade do bloco e correção do validador por meio de refinamento passo a passo. Os resultados demonstram que provas verificadas por máquina fornecem garantias de correção verificáveis além da avaliação baseada em simulação, estabelecendo um pipeline rigoroso e reproduzível de verificação que aprimora a garantia de correção e a robustez em nível de protocolo em sistemas blockchain.

Introdução

$$\rightleftharpoonup{xx}$$ $$\longleftharp{xx}$$, $$\longrightharp{xx}$$,

A tecnologia blockchain evoluiu para um paradigma de livro-razão distribuído que permite a manutenção descentralizada de registros sem depender de autoridades centralizadas. Ao replicar estados do livro razão entre os nós participantes e alcançar concordância por meio de mecanismos de consenso, os sistemas blockchain proporcionam integridade, transparência e resistência à manipulação em ambientes abertos e adversariais. Como descrito por Yaga et al.1, a arquitetura blockchain combina primitivas criptográficas, protocolos de consenso distribuídos e comunicação peer-to-peer para garantir que transações validadas se tornem computacionalmente impraticáveis de alterar. Mecanismos centrais de consenso como Prova de Trabalho (PoW) e Prova de Stake (PoS) regulam a seleção de validadores, validação de blocos e sincronização do livro-caixa. Além disso, contratos inteligentes ampliam as capacidades do blockchain ao incorporar lógica programável que executa regras pré-definidas de forma autônoma, possibilitando aplicações descentralizadas em setores como finanças, saúde e governança. À medida que as tecnologias blockchain são cada vez mais implantadas em ambientes de alto valor e críticos para segurança, garantir a correção dos mecanismos de consenso e do comportamento dos contratos inteligentes tornou-se essencial para manter a confiabilidade operacional2.

Apesar de sua natureza descentralizada, os sistemas blockchain continuam suscetíveis a vulnerabilidades lógicas e em nível protocolar. Ataques de duplo gasto podem ocorrer quando as restrições de consistência do livro-razão não são rigorosamente aplicadas. Fraquezas no nível de consenso, como lógica incorreta de seleção de validadores ou regras de validação de blocos falhas, assim como vulnerabilidades em contratos inteligentes, incluindo reentrada e controle de acesso inadequado, levaram a perdas financeiras substanciais nas plataformas implantadas. Embora os frameworks de teste empírico e simulação sejam amplamente usados para avaliar o comportamento dos protocolos PoW e PoS, essas abordagens fornecem apenas observações ilustrativas, em vez de garantias abrangentes de correção. A validação baseada em simulação não pode provar a preservação invariante em todos os estados acessíveis nem garantir propriedades de segurança e vivacidade em todos os caminhos de execução. Essa limitação destaca a necessidade de técnicas de verificação matematicamente fundamentadas que possam raciocinar rigorosamente sobre sistemas blockchain além da análise observacional.

Métodos formais oferecem essa base ao permitir a especificação e verificação do sistema por meio da lógicamatemática 3,4. O evento-B estende esse paradigma por meio de refinamento passo a passo, representando sistemas como máquinas de estados abstratas nas quais estados do sistema são limitados por invariantes e transições são modeladas como eventosprotegidos 5. A plataforma Rodin gera automaticamente obrigações de prova e suporta sua liberação, permitindo verificação verificada por máquina da preservação invariante e consistênciade estado 6. Técnicas clássicas de especificação como o B-Método7 e Z8 demonstram como o raciocínio baseado em invariantes e o refinamento formal podem garantir a correção do sistema em diferentes estágios de desenvolvimento. Esses métodos têm sido amplamente aplicados em sistemas críticos para a missão e segurança para garantir a correção antes dodesdobramento 9,10,11,12,13. Extensões adicionais como UML-B e frameworks de refinamento gráfico demonstram ainda mais a escalabilidade da modelagem baseada em refinamento para sistemas industriaiscomplexos 14,15,16,17,18,19. Esses desenvolvimentos ilustram que a modelagem formal orientada por refinamento pode gerenciar efetivamente a complexidade do sistema enquanto mantém fortes garantias de correção.

Abordagens formais de verificação também foram exploradas para sistemas blockchain. Técnicas de verificação contratual baseadas em SMT verificam automaticamente as afirmações dentro dos programas Solidity e podem produzir contraexemplos quando ocorrem violaçõeslógicas 20. Ferramentas como o VERISOL empregam abstrações de estados finitos para verificação de contratosinteligentes 2, enquanto abordagens de prova de teoremas traduzem contratos em estruturas formais de raciocínio como F*21. Além disso, formalizações semânticas da Máquina Virtual Ethereum permitem um raciocínio rigoroso sobre semântica de execução e detecçãode vulnerabilidades. De forma semelhante, ambientes de prova de teoremas como o Coq foram aplicados para analisar propriedades de segurança relacionadas ao consenso e correçãotransacional 23. Embora essas abordagens forneçam insights valiosos, elas frequentemente focam tanto na correção em nível de contrato quanto em propriedades em nível de consenso de forma independente. Invariantes do livro-razão em nível de sistema, transições de estado de consenso e comportamento de contratos inteligentes raramente são integrados em uma estrutura unificada baseada em refinamento que mantenha a rastreabilidade entre camadas de especificação e artefatos de verificação. Além disso, muitas abordagens existentes enfatizam a detecção de vulnerabilidades ou a verificação lógica de asserções, em vez da preservação sistemática invariante em múltiplos níveis de refinamento.

O presente estudo aborda essa lacuna metodológica ao propor uma estrutura unificada de verificação formal que integra a abstração de contratos inteligentes Solidity por Máquina de Estados Finitos (FSM) com modelagem de refinamento Evento-B e descarga de prova verificada por máquina na plataforma Rodin. Em vez de tratar a verificação de contratos e a modelagem por consenso como problemas separados, o framework proposto especifica formalmente transições de estado em nível de protocolo para PoW e PoS, restrições de integridade do livro-caixa, condições de unicidade de transações e evolução do estado de contratos inteligentes dentro de um único modelo estruturado. Propriedades de segurança — incluindo preservação invariante, unicidade de transações, transições de estado controladas e consistência do livro-razão — são expressas como invariantes do Evento-B e verificadas por meio de obrigações de prova geradas automaticamente. Propriedades temporais e dependentes da ordem de execução são especificadas usando a Computation Tree Logic e verificadas por meio de verificação de modelos para garantir correção além dos invariantes estáticos. Uma contribuição metodológica chave está em estabelecer rastreabilidade explícita entre camadas de abstração: funções de solidez são abstraídas em transições FSM, transições FSM são codificadas como eventos Evento-B, e invariantes juntamente com especificações temporais são diretamente ligadas a obrigações de prova liberadas e resultados de verificação de modelos. Esse mapeamento estruturado garante que cada alegação de correção seja apoiada por evidências verificadas por máquinas e distinga claramente as garantias baseadas em provas das observações baseadas em simulação.

O escopo deste trabalho é deliberadamente limitado para garantir precisão e clareza analítica. A modelagem foca em transições de estado em nível de protocolo para mecanismos de consenso, restrições de integridade do ledger, propriedades de unicidade de transações e comportamento de estado de contratos inteligentes. Aspectos em nível de rede, como atrasos na propagação de mensagens, estratégias adversariais bizantinas, mecanismos de resolução de forks e semântica detalhada de gás da Máquina Virtual Ethereum estão fora do limite de abstração definido. Ao definir explicitamente essas suposições de modelagem, o arcabouço garante que as alegações de verificação permaneçam alinhadas com as provas formalmente verificadas. O restante deste artigo apresenta a metodologia de abstração, o processo de modelagem e refinamento do Evento-B, os procedimentos para verificação invariante e temporal, e os resultados resultantes da verificação. Ao fundamentar o protocolo blockchain e a verificação de contratos inteligentes em modelagem formal baseada em refinamento e provas verificadas por máquina, este estudo fortalece o rigor metodológico e aprimora a garantia de correção pré-implantação para sistemas descentralizados de registro.

Acesso restrito. Inicie sessão ou comece um teste para visualizar este conteúdo.

Protocolo

$$\rightleftharpoonup{xx}$$ $$\longleftharp{xx}$$, $$\longrightharp{xx}$$,

Contribuições para o estudo
Neste estudo, dois contratos inteligentes Solidity foram usados como entradas de verificação. O primeiro foi um contrato no estilo Simple DAO que foi usado como estudo de caso de reentrância. O segundo era um contrato de registro afinado/transição de estado, projetado para testar restrições em nível de contrato contra gastos duplos. O código-fonte original do Solidity servia como entrada para os processos de abstração e verificação definidos neste protocolo. O processo geral de transformação usado para tais contratos é ilustrado na Figura 1, que mostra a transformação gradual do código-fonte Solidity para os modelos FSM, Evento-B e SMV durante a verificação.

Modelagem de fronteira
A modelagem formal foca na lógica de controle-fluxo de contratos inteligentes, incluindo comportamento de entrada e saída de funções, execução interna e transições de estado em nível de contrato. A visibilidade da função (pública, externa, interna e privada) foi representada juntamente com o comportamento correspondente da pilha de chamadas relevante para a análise de reentrância. Os tipos de transições abstratas (chamada, envio, transferência) eram tratados como operações para transferir éteres.

Invariantes em nível de contrato foram definidos para garantir a unicidade da transação e evitar gastos duplos dentro do limite de abstração. Para representar os requisitos de seleção de validação e integridade do bloco, a camada de abstração lógica-protocolo foi definida em termos das transições de estado em nível de protocolo tanto da Prova de Trabalho quanto da Prova de Stake.

A fronteira de abstração não incluía elementos da camada de rede, incluindo o escalonamento das mensagens a serem entregues e atrasos causados por qualquer número de saltos, resolução de fork, adversários da rede empregando estratégias bizantinas, semântica da Máquina Virtual Ethereum e semântica de gás controlada por nós de rede, propagação de exceções, execuções assíncronas, comportamento de fallback complexo e finalização em nível de rede. Assim, os resultados da determinação de dupla despesa aplicam-se apenas a invariantes em nível de contrato e não constituem um acordo de finalização em nível de rede.

Ferramentas e configuração
A plataforma Rodin foi usada para modelar, refinar, gerar obrigações de prova e executar o modelo Event-B (versão 3.7.0), que permitia que os provadores PP, ML, SMT e Atelier-B descarregassem provas automaticamente e de forma interativa. A versão 2.0.0 do nuXmv foi executada nos modelos SMV gerados em modo completo de exploração CTL para fazer verificação de modelos CTL.

Todas as execuções de verificação foram realizadas em um ambiente computacional controlado usando Ubuntu 22.04 LTS, OpenJDK 11 e Python 3.10.12. Web3 (7.6.0), NetworkX (3.4.2), Matplotlib (3.8.0), Graphviz (0.20.3), NumPy (1.26.4) e Pandas (2.2.2) foram usados para implementar elementos de simulação e visualização. Esse projeto garantia que os resultados formais de verificação e simulação pudessem ser reproduzidos quando executados sob as mesmas condições de execução.

Fluxo de trabalho de transformação
Esse processo de verificação teve quatro fases. Contratos de solidez foram inicialmente traduzidos em uma representação da Máquina de Estados Finitos (FSM-SC). O modelo FSM-SC foi posteriormente codificado no Evento-B, com invariantes e graus de refinamento claramente especificados. A abstração FSM-SC foi traduzida em um modelo SMV no nuXmv. Os resultados da verificação foram reportados como estatísticas sobre a execução da obrigação de prova e a verificação do modelo CTL, e contraexemplos foram fornecidos como casos.

Construção de FSM
Cada contrato foi abstraído como uma Máquina de Estados Finitos definida como:

figure-protocol-1

Onde:
S = conjunto de estados
S₀ = estado inicial
T = relação de transição
V = mapeamento de visibilidade
G = predicados de guarda
A = ações/atualizações de estado.

Algoritmo 1: Construção de FSM a partir da Solidez
Entrada: código-fonte Solidity
Saída: FSM-SC

1) Analisar a árvore de sintaxe abstrata do contrato de Solidity.
2) Criar o estado inicial S₀ a partir da definição do construtor.
3) Para cada função de solidez f, criar um estado de controle distinto S_f e registrar visibilidade V(f) ∈ {público, externo, interno, privado}.
4) Para cada instrução dentro da função f, derive uma transição t extraindo predicados de guarda de condições de exige/assert e ações de atualizações de variáveis de estado.
5) Adicionar a transição t a T.
6) Criar tipos explícitos de transição para operações de transferência Ether (chamada, envio, transferência), chamadas internas e externas, chamada delegada, autodestruição, uso de origem de tx, ramos condicionais e construções de loop.
7) Retorne FSM-SC = (S, S₀, T, V, G, A).

E cada função de solidez está associada a um estado de controle FSM diferente. Para compreensão de vulnerabilidades, fluxos de execução relevantes para vulnerabilidades, por exemplo, tais fluxos com chamadas externas seguidas de atualizações de balanceamento, foram explicitamente abstraídos em transições ordenadas. A Figura 2 descreve um diagrama FSM-SC de exemplo para o contrato no estilo SimpleDAO, mostrando como estados de entrada, transições de chamadas externas e sequências de atualização de estado foram abstraídos durante essa etapa de construção.

Codificação da FSM no Evento-B
A transição FSM foi representada como construtos do Evento-B. Todas as transições correspondem a eventos do Evento-B, incluindo guardas e ações específicas.

Algoritmo 2: FSM para codificação Evento-B
Entrada: FSM-SC
Saída: Máquina Evento-B e contexto

1) Definir STATE_SET e FUNÇÃO no contexto contratual.
2) Declarar variáveis que representam o estado de controle FSM e o estado em nível de contrato.
3) Representar cada estado de controle FSM s ∈ S usando current_state ∈ STATE_SET.
4) Para cada transição (s → s′, g, a), criar um evento Evento-B E_t com:
5) ONDE current_state = s ∧ g
6) ENTÃO current_state := s′ ∥ aplicar(a)
7) Codificar restrições de visibilidade usando guards derivados de V(f).
8) Definir invariantes inv1–inv9 para capturar propriedades de segurança e consistência.
9) Definir INICIALIZAÇÃO atribuindo valores S₀ e padrão.

O conjunto de estados, o estado atual, visibilidade da função, pilha de chamadas, carimbo de tempo da transação, status de transferência Ether, flag de chamada de delegado, flag de autodestruição e condição de verificação são algumas das variáveis capturadas no modelo Event-B. Os invariantes (inv1-inv9) e as ações das inicializações (act1-act6) correspondem às da especificação formal. A Figura 3 também fornece uma representação gráfica de como os eventos-chave relevantes para vulnerabilidades, especialmente transições relacionadas à reentrância, são mantidos na codificação Evento-B. Esta figura explica como os padrões estruturais do modelo FSM-SC mostrados na Figura 2 são mapeados em eventos verificáveis do Evento-B.

Estratégia de refinamento
Dois níveis de refinamento foram implementados. O fluxo de controle contratual de alto nível e os invariantes centrais foram representados no nível abstrato. O nível refinado adicionou restrições específicas de contrato, incluindo restrições de pilha de chamadas, restrições de visibilidade e condições de prevenção de reentrada.

Algoritmo 3: Refinamento e liberação de prova e obrigação
Entrada: Máquina abstrata e máquina refinada
Resultados: Obrigações e estatísticas de prova liberadas

1) Gerar obrigações de prova para a máquina abstrata em Rodin.
2) Executar provadores automáticos habilitados e registrar os resultados da descarga.
3) Gerar obrigações de prova de refinamento para a máquina refinada.
4) Aplicar avaliadores automáticos às obrigações de refinamento.
5) Cumprir as obrigações restantes de forma interativa quando necessário.
6) Estatísticas de comprovação de exportação e relatórios de status.

O relatório de prova incluiu o número de invariantes, níveis de refinamento, obrigações de prova geradas, taxa de descarga automática, taxa de descarga interativa e taxa de liberação final.

Especificação de propriedades CTL e verificação de modelos
A abstração FSM-SC foi traduzida em um modelo SMV para verificação temporal em tempo de ramificação no nuXmv.

Algoritmo 4: FSM para SMV e Verificação CTL
Saída: resultado da verificação PASS/FAIL e trilhas de contraexemplo (se houver)

1. Registrar os estados de controle FSM como um estado enumerado de variável SMV.
2. Converter transições FSM em missões próximas (de estado) protegidas.
3. Manter flags para condições relevantes à vulnerabilidade, como chamadas externas e atualizações de balanceamento.
4. Codificar propriedades CTL no nuXmv e realizar verificação de modelos.
5. Se uma propriedade falhar, gerar trilhas de contraexemplo representando sequências de transição FSM.

A verificação CTL incluía requisitos de ordem de reentrada, finalização de atualizações de estado após operações de transferência, limitação da entrada recursiva sem restrições em seções críticas e evitação de impasses.

Propriedades de segurança verificadas
O contrato no estilo Simple DAO que impede a reentrada foi confirmado garantindo ordens seguras entre chamadas externas e atualizações de estado por meio de invariantes e restrições CTL. Quando permitido, esses guardas verificavam as restrições de controle de acesso, garantindo que transições não autorizadas fossem restringidas por invariantes. O modelo do ledger reduzido verificou os invariantes da unicidade das transações e da consistência do ledger no nível de prevenção dentro do contrato.

Resultados reportados
A seção de Resultados fornece relatórios sobre métricas estruturais de FSM, métricas do modelo Evento-B e estatísticas para a verificação de prova de obrigação e CTL. Os resultados da prova formal, e os da verificação do modelo CTL, são fornecidos separadamente para distinguir a evidência de garantias de correção por invariantes e a evidência de uma verificação temporal usando verificação temporal.

Acesso restrito. Inicie sessão ou comece um teste para visualizar este conteúdo.

Resultados

$$\rightleftharpoonup{xx}$$ $$\longleftharp{xx}$$, $$\longrightharp{xx}$$,

As conclusões deste trabalho combinam os produtos formais de verificação do modelo Event-B e CTL com informações executáveis da simulação blockchain. A combinação desses resultados em múltiplas camadas apoia a validação de comportamentos-chave em contratos inteligentes, seus sistemas de consenso e suas limitações de solidez do registro dentro da exemplificação limitada do projeto.

Configuração do ambiente e verificação de dependências
O amb...

Acesso restrito. Inicie sessão ou comece um teste para visualizar este conteúdo.

Discussão

$$\rightleftharpoonup{xx}$$ $$\longleftharp{xx}$$, $$\longrightharp{xx}$$,

Verificações formais e baseadas em simulação demonstram que o sistema de verificação em múltiplas camadas usado na pesquisa era capaz de verificar o comportamento de contratos inteligentes, a correção dos mecanismos de consenso e a propriedade de integridade do livro razão sob a fronteira de abstração bem definida. O Evento-B fornece uma representação matematicamente fundamentada das propriedades de segurança, um fluxo de estado e lógica de prevenção de reentrância em termos de invariant...

Acesso restrito. Inicie sessão ou comece um teste para visualizar este conteúdo.

Divulgações

$$\rightleftharpoonup{xx}$$ $$\longleftharp{xx}$$, $$\longrightharp{xx}$$,

Os autores não têm conflitos de interesse a declarar.

Materiais

Lista de materiais utilizados neste artigo
NomeEmpresaNúmero de catálogoComentários
Rodin Platform (v3.7.0)Rodin Team / Fundação Eclipsehttps://www.event-b.org/install.htmlModelagem, refinamento e geração e liberação de Evento-B
Método Evento-BUniversidade de Southampton / Comunidade Rodinhttps://www.event-b.org/Estrutura formal de modelagem para especificação e refinamento de invariantes
NuXmv Model Checker (v2.0.0)FBK (Fondazione Bruno Kessler)https://nuxmv.fbk.eu/Verificação simbólica do modelo das propriedades CTL
Graphviz (v0.20.3)Equipe Graphvizhttps://graphviz.org/Visualização FSM e renderização de grafos
Python (v3.10.12)Fundação de Software Pythonhttps://www.python.org/downloadsAmbiente de simulação e execução
Web3.py (v7.6.0)Fundação Ethereum / Colaboradoreshttps://web3py.readthedocs.io/Interação com blockchain e simulação de transações
NetworkX (v3.4.2)Desenvolvedores NetworkXhttps://networkx.org/Modelagem de grafos de estruturas blockchain e FSM
Matplotlib (v3.8.0)Equipe de Desenvolvimento Matplotlibhttps://matplotlib.org/Plotando distribuições de tempo de mineração e validadores
NumPy (v1.26.4)Desenvolvedores NumPyhttps://numpy.org/Cálculos numéricos
Pandas (v2.2.2)Equipe de Desenvolvimento Pandashttps://pandas.pydata.org/Análise e processamento de dados
OpenJDK 11Oracle / Comunidade OpenJDKhttps://openjdk.org/projects/jdk/11/Tempo de execução necessário para a plataforma Rodin
Ubuntu 22.04 LTSCanonical Ltd.https://ubuntu.com/downloadSistema operacional para todos os experimentos
SolidezFundação Ethereumhttps://soliditylang.org/Linguagem de origem de smart contratos usada como entrada
Linguagem de Entrada (SMV) nuXmvFBKhttps://nuxmv.fbk.eu/documentation.htmlRepresentação intermediária do modelo para verificação CTL

Referências

$$\rightleftharpoonup{xx}$$ $$\longleftharp{xx}$$, $$\longrightharp{xx}$$,
  1. Yaga, D., Mell, P., Roby, N., Scarfone, K. Blockchain Technology Overview. , National Institute of Standards and Technology. Gaithersburg, MD, USA. (2018).
  2. Wang, Y., et al. Formal specification and verification of smart contracts for Azure Blockchain. arXiv preprint. , (2019).
  3. Huth, M., Ryan, M. Logic in Computer Science: Modelling and Reasoning About Systems. , Cambridge University Press. Cambridge, U.K. (2004).
  4. Baier, C., Katoen, J. P. Principles of Model Checking. , MIT Press. Cambridge, MA, USA. (2008).
  5. Abrial, J. R. Modeling in Event-B: System and Software Engineering. , Cambridge University Press. Cambridge, U.K. (2010).
  6. 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).
  7. Abrial, J. R. The B-Book: Assigning Programs to Meanings. , Cambridge University Press. Cambridge, U.K. (1996).
  8. Jacky, J. The Way of Z: Practical Programming with Formal Methods. , Cambridge University Press. Cambridge, U.K. (1996).
  9. Verma, S., Yadav, D., Chandra, G. Introduction of formal methods in blockchain consensus mechanism and its associated protocols. IEEE Access. 10, 66611-66621 (2022).
  10. 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).
  11. 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).
  12. Karmakar, R. Symbolic model checking: A comprehensive review for critical system design. Adv. Data Inf. Sci. , Springer. Singapore. 693-703 (2022).
  13. Said, M. Y., Butler, M., Snook, C. A method of refinement in UML-B. Softw. Syst. Model. 14 (4), 1557-1580 (2015).
  14. 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).
  15. 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).
  16. Morris, K. V., Snook, C. Reconciling SCXML Statechart Representations and Event-B Lower Level Semantics. , Sandia National Laboratories. Livermore, CA, USA. (2016).
  17. Butler, M. Decomposition structures for Event-B. Proc. Integrated Formal Methods (IFM 2009), , Springer. Berlin, Heidelberg. 20-38 (2009).
  18. Butler, M. Incremental design of distributed systems with Event-B. Proc. Integrated Formal Methods (IFM 2009), , Springer. Berlin, Heidelberg. (2009).
  19. Le, T. C., Garriga, M., Pautasso, C., Stankovic, M. Proving conditional termination for smart contracts. Proc. ACM Workshop Blockchains, Cryptocurrencies, and Contracts, , (2018).
  20. 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).
  21. Bhargavan, K., et al. Formal verification of smart contracts. Proc. ACM Workshop Programming Languages and Analysis for Security, , 91-96 (2016).
  22. 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).
  23. Nielsen, J. B., et al. Smart contract interactions in Coq. arXiv preprint. , (2019).

Acesso restrito. Inicie sessão ou comece um teste para visualizar este conteúdo.

Reimpressões e permissões

Solicitar permissão para reutilizar o texto ou as figuras deste artigo JoVE

Solicitar permissão

Etiquetas

Modelagem Event BProof Of WorkProof Of StakeVerifica o de Smart ContractAbstra o de M quina de EstadosProva de InvarianteVerifica o de L gica TemporalPreven o de Gasto Duplo

Artigos relacionados