上传者: wikipedia2010
|
上传时间: 2021-11-22 09:14:50
|
文件大小: 110KB
|
文件类型: -
In this tutorial we give a short introduction to the usage of the main functionalities of
NUSMV. In Chapter 2 [Examples], page 3 we describe the input language of NUSMV by
presenting some examples of NUSMV models. Chapter 3 [Simulation], page 8 shows how
the user can get familiar with the behavior of a NUSMV model by exploring its possible
executions. Chapter 4 [CTL Model Checking], page 13 and Chapter 5 [LTL Model Checking],
page 17 give an overview of BDD-based model checking, while Chapter 6 [Bounded
Model Checking], page 20 presents SAT-based model checking in NUSMV.