Formal Verification of Quasi-Synchronous Systems

Modern defense systems must be implemented as redundant, fault-tolerant systems in order to meet their reliability requirements. Unfortunately, developing protocols to achieve distributed agreement in an asynchronous environment can be deceptively difficult. Engineers often exploit the fact that their systems are quasi-synchronous, where even though the clocks of the different nodes are not synchronized, they run at the same rate, or multiples of the same rate, modulo their drift and jitter. While such designs often appear to work correctly, their intrinsic asynchrony makes them prone to latent race and deadlock conditions. This project provide systems designers with an intuitive modeling environment that 1) allows systems engineers to easily specify the high-level architecture and synchronization logic of quasi-synchronous systems using widely available system engineering notations and tools, and 2) integrates and enhances innovative formal verification tools to provide them with immediate feedback on the correctness of their designs