Lea6joijtn4qzd9bnyuk
SkillsCast

Lightning Talk: Formally Verifying Complex Systems Using TLA+

13th December 2018 in London at Business Design Centre

There are 50 other SkillsCasts available from Scala eXchange London 2018

Please log in to watch this conference skillscast.

745952363 640x360

Designing interactions across systems can be complex. Microservices, actors, threads: anything involving communication or sharing can lead to complex state machines that are then hard to test and reason about. TLA+ is a formal specification language created by Leslie Lamport (Paxos, LaTeX, Turing award) to design, model and verify systems. With it you can help uncover latent edge cases in our design, as well as prevent deadlocks and race conditions. In this short talk Ruben will share with you how you can model a real system as a PlusCal (pseudocode-like language that can be machine-translated into TLA+) algorithm, and how it compares to roughly equivalent Akka code.

YOU MAY ALSO LIKE:

Thanks to our sponsors

Lightning Talk: Formally Verifying Complex Systems Using TLA+

Ruben Berenguel

Ruben Berenguel is a senior big data engineer consultant and occasional contributor for Spark (especially PySpark). PhD in Mathematics, he moved to data engineering where he works mostly with Scala, Python and Go designing and implementing big data pipelines in London and Barcelona.

SkillsCast

Please log in to watch this conference skillscast.

745952363 640x360

Designing interactions across systems can be complex. Microservices, actors, threads: anything involving communication or sharing can lead to complex state machines that are then hard to test and reason about. TLA+ is a formal specification language created by Leslie Lamport (Paxos, LaTeX, Turing award) to design, model and verify systems. With it you can help uncover latent edge cases in our design, as well as prevent deadlocks and race conditions. In this short talk Ruben will share with you how you can model a real system as a PlusCal (pseudocode-like language that can be machine-translated into TLA+) algorithm, and how it compares to roughly equivalent Akka code.

YOU MAY ALSO LIKE:

Thanks to our sponsors

About the Speaker

Lightning Talk: Formally Verifying Complex Systems Using TLA+

Ruben Berenguel

Ruben Berenguel is a senior big data engineer consultant and occasional contributor for Spark (especially PySpark). PhD in Mathematics, he moved to data engineering where he works mostly with Scala, Python and Go designing and implementing big data pipelines in London and Barcelona.

Photos