Previous: NUSMV is open: the
To make the system more usable and improve its efficiency and its
expressiveness there are plans to introduce the following additional
- A simulation functionality, which allows the user to acquire
confidence with the correctness of the model before the
verification of the properties.
- A sequential input language. The problem with the NUSMV language is
that it is most amenable for hardware and hardware-like systems, while
its ability to model software systems is left to the user. This leaves
the user with the burden of a complex model generation activity. In
general this can be hardly acceptable, as many specification languages
(e.g., SDL) are intrinsically sequential. A possible new input
language for NUSMV is VERUS .
- Forward CTL model checking. In symbolic model checking, CTL
formulas are evaluated backward (the base operation is
EX, see Section 2). New algorithms have
been developed that allow performing evaluation of CTL
formulas via a forward state traversal . These
algorithms allow for the verification of large systems that
cannot be handled by the classical backward algorithms.
- Cone of influence reductions . The idea is to
simplify the model w.r.t. the cone of influence of the formula
to be verified, thus reducing the search space.
- Use of ``reachability don't cares'' (RDC)  to
reduce the cost of CTL model checking.
- High density reachability analysis  and under and
over approximate reachability analysis . These have
shown in some cases, together with RDC, dramatic effects in the
performance of CTL model checking.
- Optimizations for constraint-rich models , to enable
the verification of systems with complex time-invariant constraints.
Some lines of research that are currently under study and
whose results we plan to integrate inside NUSMV are specific
reduction techniques for sequential systems, a set of abstraction
techniques that implement certain heuristics developed in the theorem
proving community  and that we believe will be very
effective, the extension of CTL model checking to multi-agent systems
and security applications , and the integration of
model checking and theorem proving (SAT in particular) following
the ideas reported in  and in .