Deze studie presenteert een formeel verificatiekader voor blockchain-consensusmechanismen en smart contracts, waarbij de Event-B-methode wordt toegepast. Deze benadering combineert abstractie van representatie, invariant-gebaseerd bewijs en temporele modelcontrole met formele controles van veiligheid, levenskwaliteit en weerstand tegen dubbele uitgaven vóór implementatie.
Onderzoeksartikel
Formele verificatie van blockchain-consensusmechanismen met behulp van Event-B
In dit artikel
Samenvatting
Samenvatting
Deze studie ontwikkelt een formeel onderbouwd verificatiekader voor blockchain-consensusmechanismen en smart contract-gedrag met behulp van Event-B en het Rodin-platform. In tegenstelling tot eerdere benaderingen die voornamelijk vertrouwen op simulatie of case-based validatie van geïsoleerde contracten, integreert dit werk Finite State Machine (FSM) abstractie, invariant-gedreven bewijs, verfijningsmodellering en temporele logica-verificatie om Proof of Work (PoW), Proof of Stake (PoS) en mechanismen voor het voorkomen van dubbele uitgaven te analyseren. Solidity smart contracts worden geabstraheerd tot FSM's en gecodeerd als Event-B-machines, waardoor de formele specificatie van toestandsovergangen en veiligheidsbeperkingen mogelijk is. Veiligheidseigenschappen—waaronder transactie-uniciteit, toestandconsistentie, handhaving van toegangscontrole en grootboek-invariant behoud—worden geverifieerd via automatisch gegenereerde bewijsverplichtingen in Rodin. In totaal werden 312 bewijsverplichtingen gegenereerd, waarvan 287 (92%) automatisch werden afgekeld, en 25 interactief werden bewezen, wat resulteerde in volledige invariante dekking. Liveness-eigenschappen werden gespecificeerd in Computation Tree Logic (CTL) en gevalideerd via modelcontrole, waarbij deadlock-vrijheid werd bevestigd en uiteindelijk validatorselectie onder PoS-condities. Double-spending preventie werd formeel afgedwongen met behulp van state-consistent ledgermodeling, waarbij uniciteitsbeperkingen werden bewezen over alle bereikbare toestanden. De protocolniveau consensuslogica voor PoW en PoS werd verfijnd over drie abstractieniveaus, waarbij blokintegriteit en validatorcorrectheid werden gewaarborgd door stapsgewijze verfijning. De resultaten tonen aan dat machinegecontroleerde bewijzen verifieerbare correctheidsgaranties bieden die verder gaan dan simulatie-gebaseerde evaluatie, en zo een rigoureuze en reproduceerbare verificatiepijplijn opzetten die correctheidszekerheid en protocolniveau-robuustheid in blockchainsystemen verbetert.
Inleiding
Blockchaintechnologie is geëvolueerd tot een gedistribueerd grootboekparadigma dat gedecentraliseerde administratie mogelijk maakt zonder afhankelijk te zijn van gecentraliseerde autoriteiten. Door grootboekstaten te repliceren over deelnemende knooppunten en overeenstemming te bereiken via consensusmechanismen, bieden blockchainsystemen integriteit, transparantie en manipulatiebestendigheid in open en vijandige omgevingen. Zoals beschreven door Yaga et al.1, combineert blockchainarchitectuur cryptografische primitieven, gedistribueerde consensusprotocollen en peer-to-peer communicatie om ervoor te zorgen dat gevalideerde transacties computationeel onpraktisch worden om te wijzigen. Kernconsensusmechanismen zoals Proof of Work (PoW) en Proof of Stake (PoS) reguleren de selectie van validatoren, blokvalidatie en de synchronisatie van het grootboek. Daarnaast breiden smart contracts de mogelijkheden van blockchain uit door programmeerbare logica in te sluiten die autonoom vooraf gedefinieerde regels uitvoert, waardoor gedecentraliseerde applicaties mogelijk worden gemaakt in sectoren zoals financiën, gezondheidszorg en governance. Naarmate blockchaintechnologieën steeds vaker worden ingezet in waardevolle, veiligheidskritische omgevingen, is het waarborgen van de correctheid van consensusmechanismen en smart contract-gedrag essentieel geworden voor het behouden van operationele betrouwbaarheid2.
Ondanks hun gedecentraliseerde aard blijven blockchainsystemen vatbaar voor logische en protocolniveau-kwetsbaarheden. Double-spending aanvallen kunnen optreden wanneer de reguliere beperkingen van de grootboekconsistentie niet streng worden gehandhaafd. Zwaktes op consensusniveau, zoals onjuiste validatorselectielogica of gebrekkige blokvalidatieregels, evenals smart contract-kwetsbaarheden, waaronder re-entrancy en onjuiste toegangscontrole, hebben geleid tot aanzienlijke financiële verliezen in geïmplementeerde platforms. Hoewel empirische test- en simulatiekaders veel worden gebruikt om het gedrag van PoW- en PoS-protocollen te evalueren, bieden deze benaderingen slechts illustratieve observaties in plaats van uitgebreide garanties voor correctheid. Simulatievalidatie kan invariant behoud niet bewijzen over alle bereikbare toestanden of veiligheids- en levenskwaliteiteigenschappen garanderen onder elk uitvoeringspad. Deze beperking benadrukt de noodzaak van wiskundig onderbouwde verificatietechnieken die rigoureus kunnen redeneren over blockchainsystemen buiten de observationele analyse.
Formele methoden bieden zo'n basis door systeemspecificatie en verificatie mogelijk te maken via wiskundige logica 3,4. Event-B breidt dit paradigma uit door stapsgewijze verfijning, waarbij systemen worden weergegeven als abstracte toestandsmachines waarin systeemtoestanden worden beperkt door invarianten en overgangen worden gemodelleerd als bewaakte gebeurtenissen5. Het Rodin-platform genereert automatisch bewijsverplichtingen en ondersteunt hun afvoer, waardoor machinegecontroleerde verificatie van invariant behoud en toestandsconsistentie6 mogelijk is. Klassieke specificatietechnieken zoals de B-Methode7 en Z8 tonen aan hoe invariant-gebaseerd redeneren en formele verfijning de correctheid van het systeem kunnen waarborgen over verschillende ontwikkelingsstadia. Deze methoden zijn veelvuldig toegepast in missie-kritische en veiligheidskritische systemen om correctheid vóór de inzette waarborgen 9,10,11,12,13. Aanvullende uitbreidingen zoals UML-B en grafische verfijningkaders tonen opnieuw de schaalbaarheid van verfijningsgebaseerde modellering voor complexe industriële systemen 14,15,16,17,18,19. Deze ontwikkelingen illustreren dat verfijningsgedreven formele modellering de complexiteit van het systeem effectief kan beheren terwijl sterke garanties voor correctheid behouden blijven.
Formele verificatiebenaderingen zijn ook onderzocht voor blockchainsystemen. SMT-gebaseerde contractverificatietechnieken controleren automatisch beweringen binnen Solidity-programma's en kunnen tegenvoorbeelden opleveren wanneer logische schendingen plaatsvinden20. Hulpmiddelen zoals VERISOL maken gebruik van eindige-toestand-abstracties voor smart contract-verificatie2, terwijl theorem-bewijsbenaderingen contracten vertalen naar formele redeneerkaders zoals F*21. Daarnaast maken semantische formalisaties van de Ethereum Virtual Machine rigoureuze redenering mogelijk over uitvoeringssemantiek en kwetsbaarheidsdetectie22. Evenzo zijn theorem-bewijsomgevingen zoals Coq toegepast om consensusgerelateerde beveiligingseigenschappen en transactionele correctheid te analyseren23. Hoewel deze benaderingen waardevolle inzichten bieden, richten ze zich vaak onafhankelijk op contractniveau-correctheid of consensus-niveau eigenschappen. Grootboekinvarianten op systeemniveau, consensustoestandovergangen en smart contract-gedrag zijn zelden geïntegreerd binnen een uniform, op verfijning gebaseerd kader dat traceerbaarheid handhaaft over specificatielagen en verificatieartefacten. Bovendien leggen veel bestaande benaderingen de nadruk op kwetsbaarheidsdetectie of logische assertiecontrole in plaats van systematisch invariant behoud over meerdere verfijningsniveaus.
De huidige studie pakt deze methodologische kloof aan door een uniform formeel verificatiekader voor te stellen dat Finite State Machine (FSM)-abstractie van solidity smart contracts integreert met Event-B verfijningsmodellering en machinegecontroleerde bewijsverplichting binnen het Rodin-platform. In plaats van contractverificatie en consensusmodellering als aparte problemen te behandelen, specificeert het voorgestelde framework formeel protocolniveau-toestandsovergangen voor PoW en PoS, grootboekintegriteitsbeperkingen, transactie-uniciteitsvoorwaarden en smart contract-toestandevolutie binnen één gestructureerd model. Veiligheidseigenschappen—waaronder invariant preservation, transactie-uniciteit, gecontroleerde toestandsovergangen en grootboekconsistentie—worden uitgedrukt als Event-B invarianten en geverifieerd via automatisch gegenereerde bewijsverplichtingen. Temporele en uitvoeringsvolgorde-afhankelijke eigenschappen worden gespecificeerd met behulp van Computation Tree Logic en geverifieerd via modelcontrole om correctheid te waarborgen buiten statische invarianten. Een belangrijke methodologische bijdrage ligt in het vaststellen van expliciete traceerbaarheid over abstractielagen: soliditeitsfuncties worden geabstraheerd tot FSM-overgangen, FSM-overgangen worden gecodeerd als Event-B-gebeurtenissen, en invarianten samen met temporele specificaties zijn direct gekoppeld aan nagekomen bewijsverplichtingen en modelcontroleresultaten. Deze gestructureerde mapping zorgt ervoor dat elke correctheidsclaim wordt ondersteund door machinegeverifieerd bewijs en maakt duidelijk onderscheid tussen bewijsgebaseerde garanties en simulatiewaarnemingen.
De reikwijdte van dit werk is bewust beperkt om precisie en analytische duidelijkheid te waarborgen. Modellering richt zich op protocolniveau-toestandsovergangen voor consensusmechanismen, ledgerintegriteitsbeperkingen, transactie-uniciteitseigenschappen en het gedrag van smart contract-toestanden. Netwerkniveau-aspecten zoals berichtpropagatievertragingen, Byzantijnse adversariële strategieën, mechanismen voor fork-resolutie en gedetailleerde Ethereum Virtual Machine-gassemantiek vallen buiten de gedefinieerde abstractiegrens. Door deze modelaannames expliciet te definiëren, zorgt het kader ervoor dat verificatieclaims in lijn blijven met formeel geverifieerd bewijs. De rest van dit artikel presenteert de abstractiemethodologie, het Event-B modellerings- en verfijningsproces, de procedures voor invariante en temporele verificatie, en de resulterende verificatieresultaten. Door blockchainprotocol- en smart contract-verificatie te baseren op formeel modelleren op basis van verfijning en machinegecontroleerde bewijzen, versterkt deze studie de methodologische nauwkeurigheid en verbetert het de pre-deployment correctheidszekerheid voor gedecentraliseerde grootboeksystemen.
Toegang beperkt. Log in of start een proefperiode om deze inhoud te bekijken.
Protocol
Studieinput
In deze studie werden twee Solidity smart contracts gebruikt als verificatieinputs. Het eerste was een Simple DAO-achtige contract dat werd gebruikt als een casestudy voor re-entrancy. De tweede was een uitgedunde grootboek/statusovergangscontract bedoeld om contractniveaubeperkingen te testen tegen dubbele uitgaven. De oorspronkelijke Solidity-broncode diende als invoer voor de abstractie- en verificatieprocessen die in dit protocol zijn gedefinieerd. Het algemene transformatieproces dat voor dergelijke contracten wordt gebruikt, wordt geïllustreerd in Figuur 1, die de geleidelijke transformatie van de Solidity-broncode naar de FSM-, Event-B- en SMV-modellen tijdens verificatie toont.
Modelgrens modelleren
Formeel modelleren richt zich op de controlflowlogica van smart contracts, inclusief functionele in- en uitstapgedrag, interne uitvoering en toestandsovergangen op contractniveau. Functiezichtbaarheid (openbaar, extern, intern en privé) werd weergegeven samen met het bijbehorende call-stack gedrag dat relevant is voor re-entrancy analyse. De typen abstracte overgangen (call, send, transfer) werden behandeld als operaties voor het overdragen van ethers.
Contractniveau-invarianten werden gedefinieerd om de uniciteit van de transactie te waarborgen en dubbele uitgaven binnen de abstractiegrens te voorkomen. Om de validatieselectie- en blokintegriteitseisen te representeren, werd de protocol-logica abstractielaag gedefinieerd in termen van de protocolniveau-toestandsovergangen van zowel Proof of Work als Proof of Stake.
De abstractiegrens omvatte geen elementen van netwerklaag, waaronder het plannen van te bezorgen berichten en vertragingen veroorzaakt door een willekeurig aantal hops, fork-resolutie, netwerktegenstanders die Byzantijnse strategieën toepassen, Ethereum Virtual Machine-semantiek en gassemantiek die wordt gecontroleerd door netwerkknooppunten, excessiepropagatie, asynchrone uitvoeringen, ingewikkeld fallbackgedrag en netwerkniveau-finaliteit. De uitkomsten van dubbele uitgavenbepaling gelden dus alleen voor contractniveau-invarianten en vormen geen netwerkniveau-overeenkomst over finaliteit.
Gereedschappen en configuratie
Het Rodin-platform werd gebruikt om het Event-B (versie 3.7.0) model te modelleren, te verfijnen, te verfijnen, bewijsverplichtingen te genereren en het Event-B model te leveren, waardoor de PP-, ML-, SMT- en Atelier-B-bewijzen automatisch en interactief konden uitvoeren. nuXmv versie 2.0.0 werd uitgevoerd op de gegenereerde SMV-modellen in volledige CTL-exploratiemodus om CTL-modelcontrole uit te voeren.
Alle verificatie-uitvoeringen werden uitgevoerd in een gecontroleerde computationele omgeving met Ubuntu 22.04 LTS, OpenJDK 11 en Python 3.10.12. Web3 (7.6.0), NetworkX (3.4.2), Matplotlib (3.8.0), Graphviz (0.20.3), NumPy (1.26.4) en Pandas (2.2.2) werden gebruikt om simulatie- en visualisatie-elementen te implementeren. Dit ontwerp garandeerde dat formele verificatie- en simulatieresultaten konden worden gereproduceerd wanneer ze onder dezelfde uitvoeringsomstandigheden werden uitgevoerd.
Transformatieworkflow
Dit verificatieproces kende vier fasen. Soliditeitscontracten werden eerst vertaald naar een Finite State Machine (FSM-SC) representatie. Het FSM-SC-model werd vervolgens gecodeerd in Event-B, met duidelijk gespecificeerde invarianten en verfijningsgraden. De FSM-SC-abstractie werd vertaald naar een SMV-model in nuXmv. De verificatieresultaten werden gerapporteerd als statistieken over bewijsverplichting en CTL-modelcontrole, en tegenvoorbeelden werden als gevallen verstrekt.
FSM-constructie
Elk contract werd geabstraheerd als een eindige toestandsmachine, gedefinieerd als:
Waar:
S = verzameling toestanden
S₀ = begintoestand
T = overgangsrelatie
V = zichtbaarheidsmapping
G = wachtpredicaten
A = acties/statusupdates.
Algoritme 1: FSM-constructie uit Solidity
Invoer: Solidity-broncode
Output: FSM-SC
1) Ontleed de abstracte syntaxisboom van het Solidity-contract.
2) Skep de begintoestand S₀ uit de constructordefinitie.
3) Voor elke soliditeitsfunctie f creëer je een aparte controletoestand S_f en registreer zichtbaarheid V(f) ∈ {publiek, extern, intern, privé}.
4) Voor elke uitspraak binnen functie f leidt u een overgangsvorm t af door guardpredicaten te extraheren uit vereiste of assertieve voorwaarden en acties uit toestandsvariabelenupdates.
5) Voeg de overgangs-t toe aan T.
6) Expliciete overgangstypen creëren voor etheroverdrachtsoperaties (call, send, transfer), interne en externe calls, delegatecall, selfdestruct, tx.origin gebruik, conditionele vertakkingen en lusconstructies.
7) Geef FSM-SC = (S, S₀, T, V, G, A) terug.
En elke Solidity-functie is gekoppeld aan een andere FSM-regeltoestand. Voor het begrijpen van kwetsbaarheden werden kwetsbaarheidsrelevante uitvoeringsstromen, bijvoorbeeld dergelijke stromen met externe aanroepen gevolgd door balansupdates, expliciet geabstraheerd tot geordende overgangen. Figuur 2 beschrijft een voorbeeld van een FSM-SC-diagram voor het SimpleDAO-achtige contract, waarin wordt getoond hoe invoertoestanden, externe aanroepovergangen en toestandsupdate-sequenties tijdens deze constructiefase werden geabstraheerd.
FSM coderen in Event-B
De FSM-overgang werd weergegeven als Event-B-constructen. Alle overgangen komen overeen met Event-B-gebeurtenissen, inclusief specifieke bewakers en acties.
Algoritme 2: FSM naar Event-B codering
Invoer: FSM-SC
Output: Event-B machine en context
1) Definieer STATE_SET en FUNCTIE in de contractcontext.
2) Variabelen declareren die de FSM-controletoestand en de contractniveautoestand vertegenwoordigen.
3) Vertegenwoordig elke FSM-besturingstoestand s ∈ S met current_state ∈ STATE_SET.
4) Voor elke overgang (s → s′, g, a) maak een Event-B-gebeurtenis E_t met:
5) WAARBIJ current_state = s ∧ g
6) DAN current_state := s′ ∥ toepas(a)
7) Encodeer zichtbaarheidsbeperkingen met guards afgeleid van V(f).
8) Definieer invarianten inv1–inv9 om veiligheids- en consistentie-eigenschappen vast te leggen.
9) Definieer INITIALISATIE door S₀ en standaardwaarden toe te wijzen.
De set toestanden, de huidige toestand, functiezichtbaarheid, call stack, transactietijdstempel, Ether-overdrachtstatus, delegate call-vlag, zelfvernietigingsvlag en verificatieconditie zijn enkele van de variabelen die in het Event-B-model worden vastgelegd. De invarianten (inv1-inv9) en de acties van de initialisaties (act1-act6) komen overeen met die van de formele specificatie. Figuur 3 geeft ook een grafische weergave van hoe de belangrijkste gebeurtenissen die relevant zijn voor kwetsbaarheden, met name re-entrancy-gerelateerde overgangen, worden onderhouden in de Event-B-codering. Deze figuur legt uit hoe de structurele patronen van het FSM-SC-model zoals weergegeven in Figuur 2 worden omgezet in verifieerbare Event-B-gebeurtenissen.
Verfijningsstrategie
Er werden twee niveaus van verfijning doorgevoerd. Hoge niveau-contractcontrole-flow- en kerninvarianten werden op abstract niveau weergegeven. Het verfijnde niveau voegde contractspecifieke beperkingen toe, waaronder callstack-beperkingen, zichtbeperkingen en voorwaarden voor het voorkomen van herentrancy.
Algoritme 3: Verfijning en kwijtschelding van bewijsverplichtingen
Invoer: Abstracte machine en verfijnde machine
Output: Afgehandeld, bewijs van verplichtingen en statistieken
1) Bewijsverplichtingen genereren voor de abstracte machine in Rodin.
2) Voer ingeschakelde automatische proefmachines uit en registreer ontladingsresultaten.
3) Genereer verfijningsbestendige verplichtingen voor de verfijnde machine.
4) Automatische bewijsmiddelen toepassen op verfijningsverplichtingen.
5) Overige verplichtingen interactief nakomen wanneer dat nodig is.
6) Exportbewijsstatistieken en statusrapporten.
Bewijsrapportage omvatte het aantal invarianten, verfijningsniveaus, gegenereerde bewijsverplichtingen, automatische ontladingssnelheid, interactieve ontladingssnelheid en uiteindelijke ontladingssnelheid.
CTL-eigenschapsspecificatie en modelcontrole
De FSM-SC-abstractie werd vertaald naar een SMV-model voor vertakkingstijd-tijdverificatie in nuXmv.
Algoritme 4: FSM naar SMV en CTL Checking
Output: PASS/FAIL verificatieresultaat en tegenvoorbeeldtraces (indien aanwezig)
1. Registreer FSM-controletoestanden als een opgesomde SMV-variabeletoestand.
2. Zet FSM-overgangen om in bewaakte next(state)-opdrachten.
3. Voer vlag voor kwetsbaarheidsrelevante omstandigheden, zoals externe oproepen en saldo-updates.
4. CTL-eigenschappen coderen in nuXmv en modelcontrole uitvoeren.
5. Als een eigenschap faalt, genereer dan counterexample-traces die FSM-overgangsreeksen vertegenwoordigen.
CTL-controle omvatte vereisten voor herentrancy-orders, het afronden van state-updates na overdrachtsoperaties, het beperken van onbeperkte recursieve invoer in kritieke secties en het vermijden van deadlocks.
Beveiligingseigenschappen geverifieerd
Het Simple DAO-achtige contract dat herentrantie voorkomt, werd bevestigd door veilige ordening tussen externe oproepen en statusupdates via invarianten en CTL-beperkingen te waarborgen. Waar toegestaan, controleerden deze bewakers toegangscontrolebeperkingen, zodat ongeautoriseerde overgangen werden beperkt door invarianten. Het reduced ledger-model verifieerde de invarianten van transactie-uniciteit en grootboekconsistentie op het niveau van preventie binnen het contract.
Gerapporteerde uitkomsten
De sectie Resultaten biedt rapporten over FSM-structurele metrics, Event-B-modelmetrics en statistieken voor het bewijs van verplichting en CTL-verificatie. De resultaten van formeel bewijs, en die van CTL-modelcontrole, worden afzonderlijk gegeven om het bewijs van correctheidsgaranties door invarianten te onderscheiden, en het bewijs van tijdverificatie met temporele verificatie.
Toegang beperkt. Log in of start een proefperiode om deze inhoud te bekijken.
Resultaten
De bevindingen van dit werk combineren de formele verificatieproducten van Event-B en CTL-modelcontrole met uitvoerbare informatie uit blockchainsimulatie. De combinatie van deze meerlaagse uitgangen ondersteunt de validatie van sleutelgedrag in smart contracts, hun consensussystemen en hun beperkingen in de grootboek-degelijkheid binnen de beperkte voorbeelden van het ontwerp.
Omgevingsopstelling en afhankelijkheidsverificatie
De uitvoerin...
Toegang beperkt. Log in of start een proefperiode om deze inhoud te bekijken.
Discussie
Formele en simulatiegebaseerde verificatie tonen aan dat het meerlaagse verificatiesysteem dat in het betreffende onderzoek werd gebruikt, in staat was om het gedrag van smart contracts, de correctheid van consensusmechanismen en de ledger-integriteitseigenschap onder de goed gedefinieerde abstractiegrens te verifiëren. Event-B biedt een wiskundig onderbouwde representatie van veiligheidseigenschappen, een toestandsstroom en re-entrancy-preventielogica in termen van invarianten en op ver...
Toegang beperkt. Log in of start een proefperiode om deze inhoud te bekijken.
Openbaarmakingen
De auteurs hoeven geen belangenconflicten aan te geven.
Materialen
| Naam | Bedrijf | Catalogusnummer | Opmerkingen |
|---|---|---|---|
| Rodin Platform (v3.7.0) | Rodin Team / Eclipse Foundation | https://www.event-b.org/install.html | Event-B modelling, verfijning en generatie en afhandeling van bewijsverplichtingen |
| Event-B Method | University of Southampton / Rodin Community | https://www.event-b.org/ | Formeel modelleerkader voor invariantenspecificatie en verfijning |
| nuXmv Model Checker (v2.0.0) | FBK (Fondazione Bruno Kessler) | https://nuxmv.fbk.eu/ | Symbolische modelcontrole van CTL-eigenschappen |
| Graphviz (v0.20.3) | Graphviz Team | https://graphviz.org/ | FSM-visualisatie en grafiekweergave |
| Python (v3.10.12) | Python Software Foundation | https://www.python.org/downloads | Simulatie- en uitvoeringsomgeving |
| Web3.py (v7.6.0) | Ethereum Foundation / Contributors | https://web3py.readthedocs.io/ | Blockchain-interactie en transactiesimulatie |
| NetworkX (v3.4.2) | NetworkX Developers | https://networkx.org/ | Grafische modellering van blockchain- en FSM-structuren |
| Matplotlib (v3.8.0) | Matplotlib Development Team | https://matplotlib.org/ | Plotten van mijntijd en validatordistributies |
| NumPy (v1.26.4) | NumPy Developers | https://numpy.org/ | Numerieke berekeningen |
| Pandas (v2.2.2) | Pandas Development Team | https://pandas.pydata.org/ | Gegevensanalyse en -verwerking |
| OpenJDK 11 | Oracle / OpenJDK Community | https://openjdk.org/projects/jdk/11/ | Vereiste runtime voor Rodin-platform |
| Ubuntu 22.04 LTS | Canonical Ltd. | https://ubuntu.com/download | Besturingssysteem voor alle experimenten |
| Solidity | Ethereum Foundation | https://soliditylang.org/ | Smart contractbrontaal gebruikt als invoer |
| nuXmv Input Language (SMV) | FBK | https://nuxmv.fbk.eu/documentation.html | Tussenliggende modelrepresentatie voor CTL-verificatie |
Referenties
- 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).
Toegang beperkt. Log in of start een proefperiode om deze inhoud te bekijken.
Herprints en machtigingen
Toestemming aanvragen om de tekst of afbeeldingen van dit JoVE-artikel te hergebruiken
Toestemming aanvragen