다시보는 웨비나

Reliable by Design: Applying Formal Methods to Distributed Systems

주최자

David Turner

Yannick Welsch

주요 내용

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.

시청 에 등록

이메일을 통해 관련 내용을 보내드리겠습니다.