Towards Verified Self-Driving Infrastructure

Bingzhe Liu, Ali Kheradmand, Matthew Caesar, P. Brighten Godfrey

Research output: Chapter in Book/Report/Conference proceedingConference contribution


Modern "self-driving'' service infrastructures consist of a diverse collection of distributed control components providing a broad spectrum of application- and network-centric functions. The complex and non-deterministic nature of these interactions leads to failures, ranging from subtle gray failures to catastrophic service outages, that are difficult to anticipate and repair. Our goal is to call attention to the need for formal understanding of dynamic service infrastructure control. We provide an overview of several incidents reported by large service providers as well as issues in a popular orchestration system, identifying key characteristics of the systems and their failures. We then propose a verification approach in which we treat abstract models of control components and the environment as parametric transition systems and leverage symbolic model checking to verify safety and liveness properties, or propose safe configuration parameters. Our preliminary experiments show that our approach is effective in analyzing complex failure scenarios with acceptable performance overhead.

Original languageEnglish (US)
Title of host publicationHotNets 2020 - Proceedings of the 19th ACM Workshop on Hot Topics in Networks
PublisherAssociation for Computing Machinery
Number of pages7
ISBN (Electronic)9781450381451
StatePublished - Nov 4 2020
Event19th ACM Workshop on Hot Topics in Networks, HotNets 2020 - Virtual, Online, United States
Duration: Nov 4 2020Nov 6 2020

Publication series

NameHotNets 2020 - Proceedings of the 19th ACM Workshop on Hot Topics in Networks


Conference19th ACM Workshop on Hot Topics in Networks, HotNets 2020
Country/TerritoryUnited States
CityVirtual, Online


  • parameter synthesis
  • self-driving infrastructure
  • service infrastructure control
  • symbolic model checking
  • verification

ASJC Scopus subject areas

  • Computer Networks and Communications


Dive into the research topics of 'Towards Verified Self-Driving Infrastructure'. Together they form a unique fingerprint.

Cite this