Scribd
Upload
25 views37 pages

FM-Lect12-Spring2025-Model Checking

NuSMV is an open-source model checking tool for formal verification of hardware and software systems, ensuring that system models meet specified logical properties. An example use case involves verifying that a traffic light controller does not allow conflicting green lights by modeling it as a state machine and checking a CTL/LTL formula. The document also discusses the SMV language, variable declarations, state transitions, and LTL specifications for various examples.

Uploaded by

i200958 Sheir Muhammad
Copyright
© © All Rights Reserved
We take content rights seriously. If you suspect this is your content, claim it here.
Available Formats
Download as PDF, TXT or read online on Scribd
25 views37 pages

FM-Lect12-Spring2025-Model Checking

NuSMV is an open-source model checking tool for formal verification of hardware and software systems, ensuring that system models meet specified logical properties. An example use case involves verifying that a traffic light controller does not allow conflicting green lights by modeling it as a state machine and checking a CTL/LTL formula. The document also discusses the SMV language, variable declarations, state transitions, and LTL specifications for various examples.

Uploaded by

i200958 Sheir Muhammad
Copyright
© © All Rights Reserved
We take content rights seriously. If you suspect this is your content, claim it here.
Available Formats
Download as PDF, TXT or read online on Scribd
You are on page 1/ 37

Model Checking

NuSMV

• NuSMV (New Symbolic Model Verifier) is an open-source model checking


tool used for formal verification of hardware and software systems.

• It checks whether a given system model satisfies certain logical


specifications (properties) by exhaustively analyzing all possible states.
NuSMV model checker (SMV)

purify-primal-reverb-rise
Example

• Problem: Verify that a traffic light controller never allows two conflicting green lights (e.g., North
and East) at the same time.
• NuSMV’s Role:
• Model the traffic light system as a state machine.

• Write a CTL/LTL formula like: AG !(North_Green ∧ East_Green) ("It is always false that North
and East are green simultaneously").

• NuSMV checks if this holds; if not, it produces a counterexample showing when the error
occurs.
SMV Language
SMV Language

purify-primal-reverb-rise
SMV Programs

purify-primal-reverb-rise
Example of SMV Program

purify-primal-reverb-rise
Variable declarations

purify-primal-reverb-rise
Variable examples

purify-primal-reverb-rise
Example Using integers

purify-primal-reverb-rise
State Transitions

purify-primal-reverb-rise

// If coin inserted AND amount < 5, add 1


// If already at 5, stay at 5
// Otherwise (no coin), keep same amount
Case distinction in assignments
Case distinction in assignments
Non-determinism
Model Checking
Initial State
Assignments vs. Constraints
Assignments vs. Constraints
INIT and TRANS vs ASSIGN
LTL Specifications
Counterexamples
Module with non-determinism
Assign vs. TRANS
style
Assign vs. TRANS style

possible fix
Collatz Conjecture
Collatz Conjecture in SMV
Reminder: LTL Equivalence

Lets make SMV for it


Model checker for LTL equivalence?
Model checker for LTL equivalence $

• Use an Unconstrained model!!!


Examples for LTL equivalence

- - Distribution of operators - - Distribution of operators


LTL Specs?
LTL Specifications
MODULE main
VAR
p : boolean;
q : boolean;

-- L08, slide 33 quiz on equivalence


LTLSPEC
G F (p | q) <-> (q & G p);

LTLSPEC
G F (p | q) -> (q & G p);

LTLSPEC
(q & G p) -> G F (p | q);
Model to LTL
LTL Specifications
MODULE main
VAR
state : {s0, s1, s2};
p : boolean;
q : boolean;
r : boolean;
ASSIGN
init(state) := s0;
init(p) := TRUE;
init(q) := TRUE;
init(r) := FALSE;
next(state) := case
state = s0 : s1;
state = s1 : {s0, s2};
state = s2 : s2;
TRUE : state;
esac;

You might also like