Next:
Standard Functionalities
Up:
NUSMV: a new symbolic
Previous:
The NUSMV graphical user
System Functionalities
The functionalities provided by N
U
SMV are described below. They are grouped in standard, advanced and user functionalities.
Standard Functionalities
Encoding.
Reachability Analysis.
Fair CTL model checking.
Check for Transition Relation Totality.
Counterexamples Generation.
Advanced Functionalities
Bounded CTL.
Invariant checking.
Quantitative characteristics computation.
LTL model checking.
Partitioning of the model.
User Functionalities
Counterexample navigation.
On the fly modification of the model.
Help on line.
NuSMV
<
>
>