Cette étude présente un cadre formel de vérification pour les mécanismes de consensus blockchain et les contrats intelligents, en utilisant la méthode Événement-B. Cette approche combine abstraction à partir de la représentation, preuve basée sur des invariants et vérification temporelle du modèle avec des vérifications formelles de la sécurité, de la vivacité et de la résistance à la double dépense avant le déploiement.
Article de recherche
Vérification formelle des mécanismes de consensus blockchain utilisant Event-B
Dans cet article
Résumé
Résumé
Cette étude développe un cadre de vérification formellement fondé pour les mécanismes de consensus blockchain et le comportement des contrats intelligents en utilisant Event-B et la plateforme Rodin. Contrairement aux approches précédentes qui reposaient principalement sur la simulation ou la validation basée sur les cas de contrats isolés, ce travail intègre l’abstraction par machine à états finis (FSM), la preuve pilotée par invariants, la modélisation par raffinement et la vérification logique temporelle pour analyser la preuve de travail (PoW), la preuve de mise (PoS) et les mécanismes de prévention du double budget. Les smart contracts Solidity sont abstraits en FSM et encodés sous forme de machines Événement-B, permettant la spécification formelle des transitions d’état et des contraintes de sécurité. Les propriétés de sécurité — y compris l’unicité des transactions, la cohérence d’état, l’application du contrôle d’accès et la préservation invariante du registre — sont vérifiées grâce à des obligations de preuve générées automatiquement dans Rodin. Un total de 312 obligations de preuve ont été générées, dont 287 (92 %) ont été automatiquement annulées, et 25 ont été prouvées de manière interactive, aboutissant à une couverture totalement invariante. Les propriétés de vivacité étaient spécifiées dans Computation Tree Logic (CTL) et validées via la vérification du modèle, confirmant la liberté de blocage et la sélection finale du validateur sous conditions PoS. La prévention des doubles dépenses a été formellement appliquée à l’aide de modélisation du registre cohérent selon l’état, où les contraintes d’unicité ont été démontrées dans tous les états accessibles. La logique de consensus au niveau du protocole pour PoW et PoS a été affinée sur trois niveaux d’abstraction, garantissant l’intégrité du bloc et la correction du validateur grâce à un raffinement étape par étape. Les résultats démontrent que les preuves vérifiées par machine offrent des garanties de correction vérifiables au-delà de l’évaluation basée sur la simulation, établissant un pipeline de vérification rigoureux et reproductible qui renforce l’assurance de la correction et la robustesse au niveau des protocoles dans les systèmes blockchain.
Introduction
La technologie blockchain a évolué vers un paradigme de registre distribué qui permet une tenue décentralisée des dossiers sans recourir à des autorités centralisées. En répliquant les états du registre entre les nœuds participants et en parvenant à un accord via des mécanismes de consensus, les systèmes blockchain offrent intégrité, transparence et résistance à la falsification dans des environnements ouverts et conflictuels. Comme décrit par Yaga et al.1, l’architecture blockchain combine primitives cryptographiques, protocoles de consensus distribués et communication pair-à-pair pour garantir que les transactions validées deviennent computationnellement impraticables à modifier. Des mécanismes de consensus de base tels que la preuve de travail (PoW) et la preuve de mise (PoS) régulent la sélection des validateurs, la validation des blocs et la synchronisation du registre. De plus, les contrats intelligents étendent les capacités de la blockchain en intégrant une logique programmable qui exécute de manière autonome des règles prédéfinies, permettant des applications décentralisées dans des secteurs tels que la finance, la santé et la gouvernance. À mesure que les technologies blockchain sont de plus en plus déployées dans des environnements à forte valeur ajoutée et critiques pour la sécurité, assurer la justesse des mécanismes de consensus et du comportement des contrats intelligents est devenu essentiel pour maintenir la fiabilitéopérationnelle 2.
Malgré leur nature décentralisée, les systèmes blockchain restent vulnérables à des vulnérabilités logiques et au niveau protocolaire. Des attaques de double dépense peuvent survenir lorsque les contraintes de cohérence du registre ne sont pas strictement appliquées. Des faiblesses au niveau consensuel, telles que une logique de sélection de validateur incorrecte ou des règles de validation de blocs défaillantes, ainsi que des vulnérabilités des contrats intelligents, notamment la réentrée et un contrôle d’accès inadéquat, ont entraîné des pertes financières substantielles sur les plateformes déployées. Bien que les cadres de tests empiriques et de simulation soient largement utilisés pour évaluer le comportement des protocoles PoW et PoS, ces approches ne fournissent que des observations illustratives plutôt que des garanties de correction complètes. La validation basée sur la simulation ne peut pas prouver la préservation invariante à travers tous les états accessibles ni garantir des propriétés de sécurité et de vivacité sur chaque chemin d’exécution. Cette limitation met en lumière la nécessité de techniques de vérification fondées mathématiquement capables de raisonner rigoureusement sur les systèmes blockchain au-delà de l’analyse observationnelle.
Les méthodes formelles offrent une telle base en permettant la spécification et la vérification du système via la logiquemathématique 3,4. L’événement-B étend ce paradigme par un raffinement par étapes, représentant les systèmes comme des machines à états abstraites dans lesquelles les états du système sont contraints par des invariants et les transitions sont modélisées comme des événementsprotégés 5. La plateforme Rodin génère automatiquement des obligations de preuve et en assure le décharge, permettant une vérification par machine de la préservation invariante et la cohérencede l’état 6. Des techniques classiques de spécification telles que les méthodesB-Method 7 et Z8 démontrent comment le raisonnement basé sur les invariants et le raffinement formel peuvent garantir la correction du système à travers les différentes étapes de développement. Ces méthodes ont été largement appliquées dans des systèmes critiques pour la mission et pour la sécurité afin d’assurer leur exactitude avant le déploiement9, 10, 11, 12, 13. Des extensions supplémentaires telles que l’UML-B et les frameworks de raffinement graphique démontrent également la scalabilité de la modélisation basée sur le raffinement pour les systèmes industrielscomplexes 14, 15, 16, 17, 18, 19. Ces évolutions illustrent que la modélisation formelle axée sur le raffinement peut gérer efficacement la complexité du système tout en maintenant de fortes garanties de correction.
Des approches formelles de vérification ont également été explorées pour les systèmes blockchain. Les techniques de vérification contractuelle basées sur SMT vérifient automatiquement les assertions dans les programmes Solidity et peuvent produire des contre-exemples lorsque des violations logiques surviennent20. Des outils comme VERISOL utilisent des abstractions à états finis pour la vérification des contratsintelligents 2, tandis que les approches de démonstration de théorèmes traduisent les contrats en cadres de raisonnement formels tels que F*21. De plus, les formalisations sémantiques de la machine virtuelle Ethereum permettent un raisonnement rigoureux sur la sémantique d’exécution et la détectiondes vulnérabilités 22. De même, des environnements de démonstration de théorèmes tels que Coq ont été appliqués pour analyser les propriétés de sécurité liées au consensus et la correctiontransactionnelle 23. Bien que ces approches fournissent des perspectives précieuses, elles se concentrent souvent indépendamment soit sur la justesse au niveau du contrat, soit sur les propriétés au niveau consensuel. Les invariants du registre au niveau du système, les transitions d’état consensuel et le comportement des smart contracts sont rarement intégrés dans un cadre unifié basé sur le raffinement qui maintient la traçabilité entre les couches de spécifications et les artefacts de vérification. De plus, de nombreuses approches existantes mettent l’accent sur la détection de vulnérabilités ou la vérification logique des affirmations plutôt que sur la préservation systématique des invariants à travers plusieurs niveaux de raffinement.
La présente étude répond à cette lacune méthodologique en proposant un cadre unifié de vérification formelle qui intègre l’abstraction Finite State Machine (FSM) des smart contracts Solidity avec la modélisation de raffinement Event-B et la décharge de l’obligation de preuve vérifiée par machine au sein de la plateforme Rodin. Au lieu de traiter la vérification des contrats et la modélisation par consensus comme des problèmes distincts, le cadre proposé spécifie formellement les transitions d’état au niveau du protocole pour PoW et PoS, les contraintes d’intégrité du registre, les conditions d’unicité des transactions et l’évolution de l’état des contrats intelligents au sein d’un seul modèle structuré. Les propriétés de sécurité — y compris la préservation invariante, l’unicité des transactions, les transitions d’état contrôlées et la cohérence du registre — sont exprimées comme des invariants d’Événement-B et vérifiées par des obligations de preuve générées automatiquement. Les propriétés temporelles et dépendantes de l’ordre d’exécution sont spécifiées à l’aide de la logique de l’arbre de calcul et vérifiées par vérification du modèle afin d’assurer leur exactitude au-delà des invariants statiques. Une contribution méthodologique clé réside dans l’établissement d’une traçabilité explicite à travers les couches d’abstraction : les fonctions de solidité sont abstraites en transitions FSM, les transitions FSM sont encodées en événements Événement-B, et les invariants ainsi que les spécifications temporelles sont directement liés aux obligations de preuve déchargées et aux résultats de vérification du modèle. Cette cartographie structurée garantit que chaque affirmation de correction est étayée par des preuves vérifiées par la machine et distingue clairement les garanties basées sur la preuve des observations basées sur la simulation.
La portée de ce travail est délibérément limitée afin d’assurer la précision et la clarté analytique. La modélisation se concentre sur les transitions d’état au niveau du protocole pour les mécanismes de consensus, les contraintes d’intégrité du registre, les propriétés d’unicité des transactions et le comportement de l’état des smart contracts. Les aspects au niveau du réseau tels que les délais de propagation des messages, les stratégies adversaires byzantines, les mécanismes de résolution de fork et la sémantique détaillée des gaz de la machine virtuelle Ethereum échappent aux limites d’abstraction définies. En définissant explicitement ces hypothèses de modélisation, le cadre garantit que les affirmations de vérification restent alignées avec les preuves formellement vérifiées. Le reste de cet article présente la méthodologie d’abstraction, le processus de modélisation et d’affinement Événement-B, les procédures de vérification invariante et temporelle, ainsi que les résultats de vérification qui en résultent. En ancrant le protocole blockchain et la vérification des contrats intelligents dans la modélisation formelle basée sur le raffinement et les preuves vérifiées par machine, cette étude renforce la rigueur méthodologique et renforce l’assurance de la correction avant le déploiement pour les systèmes de registre décentralisés.
Accès restreint. Veuillez vous connecter ou commencer un essai pour afficher ce contenu.
Protocole
Contributions de l’étude
Dans cette étude, deux contrats intelligents Solidity ont été utilisés comme entrées de vérification. Le premier était un contrat de type Simple DAO utilisé comme étude de cas de réentrance. Le second était un contrat de registre allégé/transition d’État conçu pour tester les contraintes au niveau du contrat contre les doubles dépenses. Le code source original de Solidity servait d’entrée aux processus d’abstraction et de vérification définis dans ce protocole. Le processus général de transformation utilisé pour ces contrats est illustré à la Figure 1, qui montre la transformation progressive du code source Solidity dans les modèles FSM, Événement-B et SMV lors de la vérification.
Modélisation de la frontière
La modélisation formelle se concentre sur la logique de contrôle-flux des smart contracts, incluant le comportement d’entrée et de sortie des fonctions, l’exécution interne et les transitions d’état au niveau du contrat. La visibilité des fonctions (publique, externe, interne et privée) était représentée avec le comportement d’appel correspondant pertinent à l’analyse de la réentrance. Les types de transitions abstraites (appel, envoi, transfert) étaient traités comme des opérations de transfert d’ethers.
Des invariants au niveau du contrat ont été définis pour garantir l’unicité des transactions et éviter les doubles dépenses dans la frontière d’abstraction. Pour représenter les exigences de sélection de validation et d’intégrité du bloc, la couche d’abstraction logique protocolaire a été définie en fonction des transitions d’état au niveau du protocole de la preuve de travail et de la preuve de mise en jeu.
La frontière d’abstraction n’incluait pas les éléments de la couche réseau, notamment la planification des messages à livrer et les délais causés par un nombre quelconque de sauts, la résolution de fork, les adversaires du réseau employant des stratégies byzantines, la sémantique de la machine virtuelle Ethereum et la sémantique du gaz contrôlée par les nœuds réseau, la propagation des exceptions, les exécutions asynchrones, le comportement de repli complexe et la finalité au niveau du réseau. Ainsi, les résultats de la détermination des doubles dépenses ne s’appliquent qu’aux invariants au niveau du contrat et ne constituent pas un accord de finalité au niveau du réseau.
Outils et configuration
La plateforme Rodin servait à modéliser, affiner, générer des obligations de preuve et décharger le modèle Event-B (version 3.7.0), qui permettait aux indicateurs PP, ML, SMT et Atelier-B de décharger automatiquement et de manière interactive les épreuves. la version 2.0.0 de nuXmv a été exécutée sur les modèles SMV générés en mode exploration CTL complète pour effectuer la vérification des modèles CTL.
Toutes les exécutions de vérification étaient effectuées dans un environnement informatique contrôlé utilisant Ubuntu 22.04 LTS, OpenJDK 11 et Python 3.10.12. Web3 (7.6.0), NetworkX (3.4.2), Matplotlib (3.8.0), Graphviz (0.20.3), NumPy (1.26.4) et Pandas (2.2.2) ont été utilisés pour implémenter des éléments de simulation et de visualisation. Cette conception garantissait que les résultats formels de vérification et de simulation pouvaient être reproduits lors de l’exécution dans les mêmes conditions d’exécution.
Flux de travail de transformation
Ce processus de vérification comportait quatre phases. Les contrats de solidité ont d’abord été traduits en une représentation de la Machine à États Finis (FSM-SC). Le modèle FSM-SC a ensuite été encodé en Événement-B, avec des invariants et des degrés de raffinement clairement spécifiés. L’abstraction FSM-SC a été traduite en modèle SMV dans nuXmv. Les résultats de la vérification ont été présentés sous forme de statistiques sur la décharge de l’obligation de preuve et le modèle CTL, et des contre-exemples ont été fournis en cas de cas.
Construction FSM
Chaque contrat était abstrait comme une machine à états finis définie comme :
Où :
S = ensemble des états
S₀ = état initial
T = relation de transition
V = cartographie de visibilité
G = prédicats de garde
A = actions/mises à jour d’état.
Algorithme 1 : Construction FSM à partir de Solidity
Entrée : Code source Solidity
Sortie : FSM-SC
1) Analyser l’arbre syntaxique abstrait du contrat de Solidity.
2) Créer l’état initial S₀ à partir de la définition du constructeur.
3) Pour chaque fonction Solidity f, créer un état de contrôle distinct S_f et enregistrer la visibilité V(f) ∈ {public, externe, interne, privé}.
4) Pour chaque instruction dans la fonction f, dériver une transition t en extrayant des prédicats de garde à partir des conditions requise/assert et des actions issues des mises à jour des variables d’état.
5) Ajouter la transition t à T.
6) Créer des types de transition explicites pour les opérations de transfert Ether (appel, envoi, transfert), appels internes et externes, appel délégué, autodestruction, utilisation de tx.origin, branches conditionnelles et constructions de boucles.
7) Retour FSM-SC = (S, S₀, T, V, G, A).
Et chaque fonction de solidité est associée à un état de contrôle FSM différent. Pour la compréhension des vulnérabilités, les flux d’exécution pertinents pour les vulnérabilités, par exemple ces flux avec des appels externes suivis de mises à jour d’équilibre, ont été explicitement abstraits en transitions ordonnées. La figure 2 décrit un exemple de diagramme FSM-SC pour le contrat de type SimpleDAO, montrant comment les états d’entrée, les transitions d’appel externe et les séquences de mise à jour d’état ont été abstraits durant cette étape de construction.
Encodage de FSM dans l’Événement-B
La transition FSM était représentée par des constructions Événement-B. Toutes les transitions correspondent à des événements d’Événement-B, y compris des gardes et des actions particulières.
Algorithme 2 : encodage FSM vers Événement-B
Entrée : FSM-SC
Sortie : machine événement-B et contexte
1) Définir STATE_SET et FONCTION dans le contexte contractuelle.
2) Déclarer les variables représentant l’état de contrôle FSM et l’état au niveau du contrat.
3) Représenter chaque état de contrôle FSM s ∈ S en utilisant current_state ∈ STATE_SET.
4) Pour chaque transition (s → s′, g, a), créer un événement Événement-B E_t avec :
5) OÙ current_state = s ∧ g
6) ALORS current_state := s′ ∥ appliquer(a)
7) Encoder les contraintes de visibilité en utilisant des gardes dérivés de V(f).
8) Définir les invariants inv1–inv9 pour capturer les propriétés de sécurité et de cohérence.
9) Définir l’INITIALISATION en attribuant S₀ et valeurs par défaut.
L’ensemble des états, l’état actuel, la visibilité de la fonction, la pile d’appels, l’horodatage de la transaction, le statut de transfert Ether, le drapeau d’appel délégué, le drapeau d’autodestruction et la condition de vérification sont quelques-unes des variables capturées dans le modèle Événement-B. Les invariants (inv1-inv9) et les actions des initialisations (acte1-acte6) correspondent à celles de la spécification formelle. La figure 3 présente également une représentation graphique de la manière dont les événements clés pertinents pour les vulnérabilités, en particulier les transitions liées à la réentrance, sont maintenus dans l’encodage Événement-B. Cette figure explique comment les schémas structurels du modèle FSM-SC illustré à la Figure 2 sont mappés en événements Événement-B vérifiables.
Stratégie de raffinement
Deux niveaux de raffinement ont été mis en place. Les invariants de contrôle de contrôle contractuel de haut niveau et les invariants du cœur étaient représentés au niveau abstrait. Le niveau affiné a ajouté des restrictions spécifiques au contrat, notamment des restrictions de pile d’appels, des restrictions de visibilité et des conditions de prévention de la réentrée.
Algorithme 3 : Affinement et décharge de l’obligation de preuve
Entrée : Machine abstraite et machine raffinée
Résultats : obligations de preuve et statistiques de décharge
1) Générer des obligations de preuve pour la machine abstraite dans Rodin.
2) Exécuter des épreuves automatiques activées et enregistrer les résultats de décharge.
3) Générer des obligations de vérification de raffinage pour la machine affinée.
4) Appliquer des mesures automatiques aux obligations de raffinement.
5) Remplir les obligations restantes de manière interactive lorsque cela est nécessaire.
6) Statistiques de preuve d’exportation et rapports d’état.
La déclaration de preuves comprenait le nombre d’invariants, les niveaux de raffinement, les obligations de preuve générées, le taux de décharge automatique, le taux de décharge interactive et le taux de décharge final.
Spécification des propriétés CTL et vérification des modèles
L’abstraction FSM-SC a été traduite en un modèle SMV pour la vérification temporelle en temps de branchement dans nuXmv.
Algorithme 4 : Vérification FSM vers SMV et CTL
Sortie : résultat de vérification PASS/FAIL et traces contre-exemples (le cas échéant)
1. Enregistrer les états de contrôle FSM comme un état énuméré de variables SMV.
2. Convertir les transitions FSM en missions prochaines (état) protégées.
3. Maintenir des indicateurs pour les conditions pertinentes à la vulnérabilité, telles que les appels externes et les mises à jour d’équilibre.
4. Coder les propriétés CTL dans nuXmv et effectuer la vérification des modèles.
5. Si une propriété échoue, générez des traces contre-exemples représentant les séquences de transition FSM.
La vérification CTL comprenait les exigences d’ordre de réentrée, la finalisation des mises à jour d’état après les opérations de transfert, la limitation de l’entrée récursive non contrainte dans les sections critiques et l’évitement des blocages.
Propriétés de sécurité vérifiées
Le contrat de type Simple DAO qui empêche la réentrée a été confirmé en assurant un ordre sûr entre appels externes et mises à jour d’état via des invariants et des contraintes CTL. Lorsque cela était permis, ces agents vérifiaient les contraintes de contrôle d’accès, s’assurant que les transitions non autorisées étaient restreintes par des invariants. Le modèle du registre réduit a vérifié les invariants de l’unicité des transactions et de la cohérence du registre au niveau de prévention dans le contrat.
Résultats rapportés
La section Résultats fournit des rapports sur les métriques structurelles FSM, les métriques du modèle Événement-B, et les statistiques pour la preuve d’obligation et la vérification CTL. Les résultats de la preuve formelle, ainsi que ceux de la vérification par modèle CTL, sont donnés séparément pour distinguer la preuve de garanties de correction par les invariants, et la preuve d’une vérification temporelle utilisant la vérification temporelle.
Accès restreint. Veuillez vous connecter ou commencer un essai pour afficher ce contenu.
Résultats
Les résultats de ce travail combinent les produits de vérification formelle de la vérification des modèles Event-B et CTL avec des informations exécutables issues de la simulation blockchain. La combinaison de ces sorties multi-couches permet de valider les comportements clés dans les contrats intelligents, leurs systèmes de consensus et leurs limitations de solidité du registre dans l’exemplification limitée de la conception.
Configuration de l’enviro...
Accès restreint. Veuillez vous connecter ou commencer un essai pour afficher ce contenu.
Discussion
La vérification formelle et basée sur la simulation démontre que le système de vérification à plusieurs niveaux utilisé dans la recherche donnée était capable de vérifier le comportement des contrats intelligents, la correction des mécanismes de consensus et la propriété d’intégrité du registre sous la frontière d’abstraction bien définie. L’événement-B fournit une représentation mathématiquement fondée sur les propriétés de sécurité, une logique de flux d’état et de prévention de la rée...
Accès restreint. Veuillez vous connecter ou commencer un essai pour afficher ce contenu.
Déclarations de divulgation
Les auteurs n’ont aucun conflit d’intérêts à déclarer.
Matériaux
| Nom | Entreprise | Numéro de catalogue | Commentaires |
|---|---|---|---|
| Plateforme Rodin (v3.7.0) | Équipe Rodin / Fondation Eclipse | https://www.event-b.org/install.html | Modélisation événement-B, affinement, ainsi que génération et décharge d’obligations de preuve |
| Méthode événement-B | Université de Southampton / Communauté de Rodin | https://www.event-b.org/ | Cadre de modélisation formelle pour la spécification et le raffinement des invariants |
| nuXmv Model Checker (v2.0.0) | FBK (Fondazione Bruno Kessler) | https://nuxmv.fbk.eu/ | Vérification symbolique des propriétés CTL par modèle |
| Graphviz (v0.20.3) | Équipe Graphviz | https://graphviz.org/ | Visualisation FSM et rendu de graphes |
| Python (v3.10.12) | Fondation Python Software | https://www.python.org/downloads | Environnement de simulation et d’exécution |
| Web3.py (v7.6.0) | Fondation Ethereum / Contributeurs | https://web3py.readthedocs.io/ | Interaction blockchain et simulation de transactions |
| NetworkX (v3.4.2) | Développeurs NetworkX | https://networkx.org/ | Modélisation graphique des structures blockchain et FSM |
| Matplotlib (v3.8.0) | Équipe de développement Matplotlib | https://matplotlib.org/ | Tracé du temps de minage et des distributions des validateurs |
| NumPy (v1.26.4) | Développeurs NumPy | https://numpy.org/ | Calculs numériques |
| Pandas (v2.2.2) | Équipe de développement Pandas | https://pandas.pydata.org/ | Analyse et traitement des données |
| OpenJDK 11 | Oracle / Communauté OpenJDK | https://openjdk.org/projects/jdk/11/ | Durée d’exécution requise pour la plateforme Rodin |
| Ubuntu 22.04 LTS | Canonical Ltd. | https://ubuntu.com/download | Système d’exploitation pour toutes les expériences |
| Solidité | Fondation Ethereum | https://soliditylang.org/ | Langage source des contrats intelligents utilisé en entrée |
| Langage d’entrée nuXmv (SMV) | FBK | https://nuxmv.fbk.eu/documentation.html | Représentation intermédiaire du modèle pour la vérification CTL |
Références
- 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).
Accès restreint. Veuillez vous connecter ou commencer un essai pour afficher ce contenu.
Réimpressions et autorisations
Demander l’autorisation de réutiliser le texte ou les figures de cet article JoVE
Demander une autorisation