本页内容尚不支持所选语言。Elastic 正在不断努力,以实现对多种语言内容的支持。感谢您在此期间给予的耐心与陪伴!

On-demand webinar

Reliable by Design: Applying Formal Methods to Distributed Systems

Hosted by:

David Turner

Yannick Welsch

Overview

Building fast, scalable, and robust distributed systems such as Elasticsearch requires choosing the right algorithms for the right tasks. While many algorithms are readily available, often they need to be extended or adapted to fit the requirements of a real-world implementation. For instance, customizing or combining algorithms in non-trivial ways can easily break safety properties. Using formal methods in the development process of a distributed system helps to catch bugs in the design phase and reveal fundamental issues that testing might not easily uncover.

Learn how the Elasticsearch team is making use of formal methods in the design of distributed algorithms. They'll discuss their specification methodology, toolset, and their experiences applying it to the data replication and cluster consensus algorithms in Elasticsearch. In particular, they'll focus on their recent work on these two core algorithms using the TLA+ toolbox (based on Lamport's Temporal Logic of Actions) and the Isabelle/HOL theorem prover system.

Register to watch

You'll also receive an email with related content.

MarketoFEForm

提交即表示您确认您已阅读并同意我们的服务条款,并且 Elastic 可以根据您提供的联系方式与您联系,以向您介绍我们的相关产品和服务。要了解更多信息或随时退出,请参阅 Elastic 的隐私声明