The SMV system is a tool for checking finite state system against specifications in the temporal logic CTL. The input language of SMV is designed to allow the description of finite state system that range from completely synchronous to completely asynchronous and from the detailed to the abstract. One can readily specify a system as a synchronous Mealy machine or as an asynchronous network of abstract, nondeterministic processes. The language provides for modular hierarchical descriptions, and for the definition of reusable components. Since it is intended to describe finite state machines, the only data types in the language are finite ones. Booleans, scalars and fixed arrays. Static, structured data types can also be constructed. The logic CTL allows a rich class of temporal properties, including safety, livenesss, fairness and deadlock freedom, to be specified in a concise syntax. SMV uses the OBDD-based symbolic model checking algorithm to efficiently determine whether specifications expressed in CTL are satisfied.
Keywords for this software
References in zbMATH (referenced in 10 articles )
Showing results 1 to 10 of 10.
- Kamkin, A.S.: Projecting transition systems: overcoming state explosion in concurrent system verification (2015)
- Gao, Xinyan; Zhou, Ning; Wu, Jinzhao; Li, Dakui: Wu’s characteristic set method for SystemVerilog assertions verification (2013)
- Tanner, Herbert G.; Fu, Jie; Rawal, Chetan; Piovesan, Jorge L.; Abdallah, Chaouki T.: Finite abstractions for hybrid systems with stable continuous dynamics (2012)
- Girard, Antoine; Pappas, George J.: Approximate bisimulation: a bridge between computer science and control theory (2011)
- Donzé, Alexandre; Krogh, Bruce; Rajhans, Akshay: Parameter synthesis for hybrid systems with an application to Simulink models (2009)
- Julius, A.Agung; Pappas, George J.: Trajectory based verification using local finite-time invariance (2009)
- Ratschan, Stefan; Smaus, Jan-Georg: Finding errors of hybrid systems by optimising an abstraction-based quality estimate (2009)
- Lerda, Flavio; Kapinski, James; Clarke, Edmund M.; Krogh, Bruce H.: Verification of supervisory control software using state proximity and merging (2008)
- Baldamus, Michael; Schröder-Babo, Jochen: p2b: A translation utility for linking Promela and symbolic model checking (tool paper) (2001)
- Clarke, E.M.; Emerson, E.A.; Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications (1986)
Further publications can be found at: http://www.cs.cmu.edu/~modelcheck/pubs.htm