Formalism-Driven Development of Decentralized Systems
Yepeng Ding, Hiroyuki Sato

TL;DR
This paper introduces a formalism-driven development process and a supporting framework for creating correct decentralized systems, addressing challenges in ensuring their reliability and security.
Contribution
It proposes an iterative development process guided by formal methods and introduces the Seniz framework with a new modeling language for practical application.
Findings
Successful case studies demonstrating FDD's effectiveness
Enhanced assurance of correctness in decentralized systems
Practical framework with modeling language and scaffolds
Abstract
Decentralized systems have been widely developed and applied to address security and privacy issues in centralized systems, especially since the advancement of distributed ledger technology. However, it is challenging to ensure their correct functioning with respect to their designs and minimize the technical risk before the delivery. Although formal methods have made significant progress over the past decades, a feasible solution based on formal methods from a development process perspective has not been well developed. In this paper, we formulate an iterative and incremental development process, named formalism-driven development (FDD), for developing provably correct decentralized systems under the guidance of formal methods. We also present a framework named Seniz, to practicalize FDD with a new modeling language and scaffolds. Furthermore, we conduct case studies to demonstrate the…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsModel-Driven Software Engineering Techniques · Advanced Software Engineering Methodologies · Business Process Modeling and Analysis
