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. We 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 runtime. 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.