形式主义驱动的去中心化系统开发
Formalism-Driven Development of Decentralized Systems
摘要：
去中心化系统已经被广泛开发和应用，以解决中心化系统中的安全和隐私问题，特别是自分布式账本技术的发展以来。然而，在交付之前确保其设计正确运作并尽量减少技术风险是一项挑战。虽然形式化方法在过去的几十年里取得了显著的进步，但从开发过程的角度来看，基于形式化方法的可行解决方案还没有得到很好的开发。在本文中，我们制定了一个迭代和增量的开发过程，命名为形式主义驱动的开发（FDD），开发可证明正确的分散系统的指导下，正式的方法。我们还提出了一个名为Seniz的框架，实践FDD与一个新的建模语言和脚手架。此外，我们进行案例研究，以证明FDD在实践中的有效性与Seniz的支持。
英文摘要：
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 effectiveness of FDD in practice with the support of Seniz.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
