论文标题
形式主义驱动的分散系统的发展
Formalism-Driven Development of Decentralized Systems
论文作者
论文摘要
分散的系统已被广泛开发和应用，以解决集中式系统中的安全和隐私问题，尤其是自分布式分类帐技术的发展以来。但是，确保其在设计方面的正确功能并在交付前将技术风险降至最低是一个挑战。尽管在过去的几十年中，正式的方法取得了重大进展，但从发展过程的角度来看，基于正式方法的可行解决方案并没有得到很好的发展。在本文中，我们制定了一个迭代和增量发展过程，称为形式主义驱动的发展（FDD），用于在形式方法的指导下开发可证明正确的分散系统。我们还提出了一个名为Seniz的框架，以用新的建模语言和脚手架实用FDD。此外，我们进行案例研究以证明在Seniz的支持下实践中FDD的有效性。
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.
