Compiling Distributed System Models into Implementations
Ivan Beschastnikh
Associate Professor in the Department of Computer Science University
British Columbia
DEIB - Meeting Room (building 22)
November 29th, 2019
2.30 pm
Contacts:
Luciano Baresi
Research Line:
Advanced software architectures and methodologies
Associate Professor in the Department of Computer Science University
British Columbia
DEIB - Meeting Room (building 22)
November 29th, 2019
2.30 pm
Contacts:
Luciano Baresi
Research Line:
Advanced software architectures and methodologies
Abstract
Distributed systems are difficult to design and implement correctly. In response, both research and industry are exploring applications of formal methods to distributed systems. For example, Amazon has reported using TLA+ and PlusCal to verify its web services. A key challenge in this domain is the missing link between the formal design of a system and its implementation. Today, this link is bridged through manual and error-prone developer effort. In this talk I will first present a language called Modular PlusCal (MPCal) that extends PlusCal by separating the model of the system from a model of the environment. I will then present a compiler toolchain called PG that translates MPCal models to TLA+ for model checking, and also compiles MPCal models to executable Go code. In this way, system designers can use MPCal to model and verify their distributed system designs, and can then use PGo to extract working implementations of these designs.
Short Bio
Ivan Beschastnikh is an Associate Professor in the Department of Computer Science at the University of British Columbia. He finished his PhD at the University of Washington in 2013 and received his formative training at the University of Chicago. He has broad research interests that touch on systems and software engineering. His recent projects span distributed systems, program analysis, networks, and security. Visit his homepage to learn more: http://www.cs.ubc.ca/~bestchai/