5. Results and Future Directions

NUSMV is a robust, well structured and flexible platform, designed to be applicable in technology transfer projects. The performance of NUSMV have been compared with those of SMV by running a number of SMV examples. Despite the fact that NUSMV gives up some of the optimizations of SMV to simplify the dependencies between modules, an improvement in computation time has been obtained. In most examples NUSMV performs better than SMV, in particular for larger examples. This enhancement in performance is mainly due to the use of CUDD BDD package.

The NUSMV architecture provides a precise distinction between the front-end, specific to the SMV input language, and the back-end (including the heuristics for model partitioning and model checking algorithms), which is independent of the input language. This separation has been used to develop on top of NUSMV the MBP system. MBP is a planner able to synthesize reactive controllers for achieving goals in nondeterministic domains [4].

Functionalities currently under development are a simulator, which is of paramount importance for the user to acquire confidence in the correctness of the model, and a compiler for an imperative style input language, which can often be very convenient in the modeling process. Further developments will include the integration of decomposition techniques (e.g. abstraction and compositional verification), and new and very promising techniques based on the use of efficient procedures for propositional satisfiability, following the ideas reported in [1].