Future Directions

To make the system more usable and improve its efficiency and its expressiveness there are plans to introduce the following additional functionalities.

• 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 [13].
• 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 [43]. These algorithms allow for the verification of large systems that cannot be handled by the classical backward algorithms.
• Cone of influence reductions [3]. 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) [63] to reduce the cost of CTL model checking.
• High density reachability analysis [54] and under and over approximate reachability analysis [48]. These have shown in some cases, together with RDC, dramatic effects in the performance of CTL model checking.
• Optimizations for constraint-rich models [62], 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 [38] and that we believe will be very effective, the extension of CTL model checking to multi-agent systems and security applications [2], and the integration of model checking and theorem proving (SAT in particular) following the ideas reported in [36] and in [5].