Formal Verification of Quasi-Synchronous Systems
Final rept. Jan 2013-Jan 2015
ROCKWELL COLLINS INC CEDAR RAPIDS IA
Pagination or Media Count:
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.
- Computer Programming and Software
- Computer Systems