DejaVu(NPO-50864-1)

The objective of DejaVu is to verify the execution of a running system against a requirement formalized in a formal logic. The system will typically be a software system that has been instrumented to generate events as it executes. The event stream is then consumed by the DejaVu monitor, and checked against a formal specification. If the event stream violates the specification, an error message is generated. This technology can be used in two ways: online and offline. In the online case, it runs on board for example a rover as it operates, checking that what is happening on the rover is according to expectations formalized in the formal logic. If the expectations are not met, the DejaVu monitor will inform the software that it needs to correct behavior. Alternatively, DejaVu can be used to analyze log files produced by the monitored system. Such log files can be analyzed after the system has executed.Software program for analyzing execution traces generated by a running system, typically another program, here referred to as the Monitored System (MS). The MS must be instrumented to emit events as it executes. The emitted trace is consumed by the DejaVu monitor, which verifies it against a property (requirement) formalized in first-order past time temporal logic. The system is innovative in using BDDs (Binary Decision Diagrams) for storing data from the execution trace.