Symbolic Model Verifier
The Symbolic Model Verifier ( SMV ) is a tool to model checking ( English Model Checking ). This model checker checks finite state machines (Engl. Finite state machines ) to the temporal logic CTL .
technology
The input language allows a machine to be described synchronously, asynchronously, in detail or abstractly. In the language there are only finite data types , i.e. Boolean variables , scalar variables and fixed arrays . However, static, structured data types can be created.
CTL supports the precise definition of temporal properties such as safety, liveliness, fairness or freedom from deadlocks . To test the models, SMV uses a symbolic algorithm based on ordered binary decision diagrams (OBDD).
Input file
The input file contains the description of the state machine and the requirements specification in the input language of SMV.
Representation of states
The states are represented by enumerations . The behavior can be specified non-deterministically . Uninitialized variables correspond to (external) events. They can be checked during the model checking. With SMV, the system model can be divided into several modules. These modules are used to improve understanding and to model interactions between system components.
Interactions between system components
The interaction between the system components can take place synchronously or asynchronously. Synchronous means, for example, that all modules are concurrently oriented to one cycle. With asynchronous execution, the processes have different execution times.
During verification , fairness can be enforced by restricting the test to certain execution paths along which a formula is infinitely true. In this way, fair access to resources can be enforced. A resource is not permanently withdrawn from any of the processes.
Current version
The last release of SMV is version 2.5 for Windows NT from 1998. The Model Checker runs on SunOS 5, Solaris , Linux , Ultrix .
NuSMV
NuSMV was developed as an updated version of SMV in a joint project by ITC-IRST ( Istituto Trentino di Cultura, Istituto per la Ricerca Scientifica e Tecnologica in Trient ), Carnegie Mellon University , the University of Genoa and the University of Trento . It is a new implementation and extension of SMV. NuSMV supports model checking by means of a SAT solver . It was designed as an open architecture and is widely used in other projects.
NuSMV-2 has been released as open source software under the LGPL .
The latest version of NuSMV (2.4.3) was announced on May 22, 2007. NuSMV-2 can be compiled under most common operating systems that support the POSIX standard . A Windows installer is also offered on the website .
literature
- Béatrice Bérard, Michel Bidoit, Alain Finkel: Systems and Software Verification: Model-Checking Techniques and Tools . Springer, 2001, ISBN 3-540-41523-8
Web links
Individual evidence
- ↑ NuSMV: a new symbolic model checker ( Memento from June 19, 2010 in the Internet Archive )