公开(公告)号：US20240241889A1

公开(公告)日：2024-07-18

申请号：US18097670

申请日：2023-01-17

Applicant: VMware, Inc.

Inventor： Lalith Suresh ,  Xudong Sun ,  Adriana Szekeres

IPC: G06F16/28

CPC classification number: G06F16/285

Abstract: Examples described herein include systems and methods for providing a framework for building and verifying cluster-management controllers. Using this framework, a developer can submit only a fraction of the code otherwise required to verify safety and liveness of a controller. A verification framework is provided that can verify the implementation of a cluster-management controller down to the manner it will execute. The developer can submit a small function that runs inside the provided framework, making formal verification possible. The framework provided to the developer can incorporate the complex details regarding standard portions of cluster-management controllers, the underlying platform (such as KUBERNETES, as an example), platform API, platform networking, and so on. The developer's code can therefore focus on the new features but still make use of formal verification for how that code will work within an entire cluster-management system.