The SMV specification language

The current NUSMV input language [19] is essentially the same as the CMU SMV input language [47,26]. The NUSMV input language is designed to allow for the description of finite state systems. The only data types provided by the language are booleans, bounded integer subranges, and symbolic enumerated types. Moreover, NUSMV allows for the definitions of bounded arrays of basic data types.

The description of a complex system can be decomposed into modules, and each of them can be instantiated many times. This provides the user with a modular and hierarchical description, and supports the definition of reusable components. Each module defines a finite state machine. Modules can be composed either synchronously or asynchronously using interleaving. In synchronous composition a single step in the composition corresponds to a single step in each of the components. In asynchronous composition with interleaving a single step of the composition corresponds to a single step performed by exactly one component. The NUSMV input language allows to describe deterministic and non deterministic systems.

A NUSMV program can describe both the model and the specification. Figure 4 gives a small example of a NUSMV program. The example in Figure 4 is a model of a 3 bit binary counter circuit. It illustrates the definition of reusable modules and expressions.

  

Figure 4: A simple NuSMV program.

The module counter_cell is instantiated three times, with names bit0, bit1 and bit2. The module counter_cell has a formal parameter carry_in. In the instantiation of the module, actual signals (1 for the instance bit0, bit0.carry_out for the instance bit1 and bit1.carry_out for the instance bit2) are plugged in for the formal parameters, thus linking the module instance to the program (a module can be seen as a subroutine). The property that we want to check is ``invariantly eventually the counter count till 8'' which is expressed in CTL using the design state variables as ``AG AF bit2.carry_out''.

It is also possible to specify the transition relation and the set of initial states of a module by means of propositional formulas, using the keywords TRANS, and INIT respectively. This provides the user with a lot of freedom in designing systems. In Figure 5 there is an equivalent definition of module counter_cell using propositional formulas.

  

Figure 5: An equivalent definition of module counter_cell of the example described in Figure 4.

With respect to CMU SMV, the input language of NUSMV has been extended to allow for the specification of properties expressed in LTL and the specifications of invariants [19].