Zenet: Generating and Enforcing Real-Time Temporal Invariants
Generating correct specifications for real-time event-driven software systems is difficult and time-consuming. Even when such specifications have been created, they are often used to guide development rather than state properties guaranteed by the actual system. The authors propose a specification generator that reads execution traces and can generate invariants with real-time constraints. That specification can also offer programmers the ability to repair violated invariants at run-time. Creating fault-tolerant systems in this manner would provide software engineers guarantees about the software's high-level operation and its ability to recover from errors.