|
NuSMV is a reimplementation and extension of SMV symbolic model checker, the first model checking tool based on Binary Decision Diagrams (BDDs).〔K.L. McMillan. Symbolic model checking. In Kluwer Academic Publ.,1993.〕 The tool has been designed as an open architecture for model checking. It is aimed at reliable verification of industrially sized designs, for use as a backend for other verification tools and as a research tool for formal verification techniques. NuSMV has been developed as a joint project between ITC-IRST (Istituto Trentino di Cultura in Trento, Italy), Carnegie Mellon University, the University of Genoa and the University of Trento. NuSMV 2, version 2 of NuSMV, inherits all the functionalities of NuSMV. Furthermore, it combines BDD-based model checking with SAT-based model checking.〔A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without bdds. In Tools and Algorithms for Construction and Analysis of Systems, In TACAS’99, March 1999.〕 It is maintained by (Fondazione Bruno Kessler ), the successor organization of ITC-IRST. == Functionalities == NuSMV supports the analysis of specifications expressed in CTL and LTL. User interaction is performed with a textual interface, as well as in batch mode. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「NuSMV」の詳細全文を読む スポンサード リンク
|