date/vreme: 14/05/2024, 11h
venue/mesto: NTP 503 (V floor)
Speaker / Predavač
Dr. Pavle Subotic, Fantom Foundation
https://psubotic.github.io/ (home page)
Title / Naslov:
Towards Formal Model Driven Development for Blockchains
Abstract / Sažetak:
Blockchains are the core technology behind Decentralized Finance( DeFi), a technology changing how financial services are accessible, managed, and implemented. Blockchains operate by maintaining a network of public validator nodes that communicate together in order to consistently replicate the history of transactions that have occurred on the blockchain. Moreover, the blockchain needs to maintain this consistency among node crashes and malicious actors. However, the distributed nature of the blockchain makes software not only difficult to design but also difficult to test. Furthermore, the fact that the blockchain is public, it is difficult to enforce that patches are installed on all nodes. In this talk, I describe ongoing work into a rigorous yet practical development process for blockchains. Our process is driven by a model described by a formal specification that is proven to be safe. From the specification, we generate execution traces from a model checker that become test cases for an implementation in a simulated environment. Our specification is designed to be modular and reusable, thus making this process lightweight for improvements to blockchain protocols.