NuSMV 2 5 Tutorial Roberto Cavada Alessandro Cimatti Gavin Keighren Emanuele Olivetti Marco Pistore and Marco Roveri FBK irst Via Sommarive 18 38055 Povo Trento Italy Email nusmv fbk eu Contents 1 Introduction 2 Examples 2 1 Synchronous Systems 2 1 1 Single Process Example 2 2 Asynchronous Systems 2 2 1 Inverter Ring 2 2 2 Mutual Exclusion 2 3 Direct Specification 3 Simulation 3 1 Trace
NuSMV 2 5 User Manual Roberto Cavada Alessandro Cimatti Charles Arthur Jochim Gavin Keighren Emanuele Olivetti Marco Pistore Marco Roveri and Andrei Tchaltsev FBK irst Via Sommarive 18 38055 Povo Trento Italy Email This document is part of the distribution package of the NUSMV model checker available athttp nusmv fbk eu Parts of this documents have been taken from The SMV System Draft by K McMillan available at sdfdsf http www cs cm