Up: System Architecture
Previous: Explanation module.
The LTL module is a separate module that calls an external program
that translates the LTL formula into a tableau suitable to be loaded
into NUSMV. This program also generates a new CTL formula to be
verified on the synchronous product of the original system and the
generated tableau. This module was plugged in on top of the other
modules (e.g., the Parser, the Encoder, the FSM Compiler, the Model
Checking and the Explanation modules), thus reusing a lot of the
functionalities already present in the architecture.