symbolic model checker

XChek
symbolic model checker
from University of Toronto
Labs in Module: 6CCS3VER SEM1
TA: Karine Even-Mendoza
karine.even_mendoza@kcl.ac.uk
October 2019
Starting Up XChek
• Starting Xchek
• Applications à Programming à Xchek
• Application menu on the upper-left side
of your screen
• Load GCLang Models
• File àOpen model
• Pick a model compiler: GCLang Compiler
• Properties tab: GCLang File
• Select a file with a model
• E.g., opt/xchek/examples/gclang/peterson_bool.gc
• After loading: compiled in 0.05s + loaded
• We only use Boolean models in the labs! Taken from χChek RC2 User Manual
http://www.cs.toronto.edu/~arie/xchek/xchek_user_manual.pdf
Models – GCLang: example
• Model’s name
• Variables definition (only Booleans!)
• Initialize the variable – init. states definition
• — for comments!
Models – GCLang: example
• RULES – describe the model itself
• Syntax –
guard : new state
Logical Connectors and Constants in XChek

• True:
• “T” in the query
• “true” in the model
• False:
• “F” in the query
• “false” in the model
• Data-type: “boolean” (e.g., s : boolean;)
Verifying the Model
• Temporal logic: use CTL
• Try for example:
EF (pc10=T ∧ pc11 = T ∧ pc20 = T ∧ pc21 = T)
EF ((pc10=T ∧ pc11 = T) ∨ (pc20 = T ∧ pc21 = T))
EF (y1 = T ∧ y2 = T)
AG ((s=F) -> EF(s=T))
EF ((s=F) -> EX(s=T))
• Can you guess what the model you’ve
loaded does?
• Can you write your own CTL formulas?
• Download at home:
http://www.cs.toronto.edu/~arie/xchek/ Taken from http://www.cs.toronto.edu/~arie/xchek/xchek_user_manual.pdf χChek RC2 User Manual
CTL properties with some explanations
— (1) False and (2) True
— 1. By looking at all possible guard and the changes apply once the guard is true, you can see when it sets the values of s,y1, and y2:
— Thus the guard of pc10=TT and pc20==TT is pc1=10 and pc2=10 respectively, but also depends on the values of s,y1 and y2.
— If pc1 start (s=1) and set the flag y1 then pc2 cannot be changed to 11 till pc1 released the flag y1 (and vice versa).
EF (pc10=T ∧ pc11 = T ∧ pc20 = T ∧ pc21 = T)
— 2. But this can be just fine
EF ((pc10=T ∧ pc11 = T) ∨ (pc20 = T ∧ pc21 = T))
— True (all)
— From the initial state the two guards pc1=TF and pc2=TF are true, if we apply these actions both (one after another), then the 3rd state will true for
this ctl
— But, only one can step into “critical area/code”, which is the last to set s (or to set its flag y).
EF (y1 = T ∧ y2 = T)
— If s is set to false at some point it can be true, and there is a state where it happens (and also for the other case T to F), that is always pc1 or pc2 can
try to perform the critical code
AG ((s=F) -> EF(s=T))
EF ((s=F) -> EX(s=T))
— True, there is a loop of 3 edges back to the init state
AG ((s = F ∧ y1 = F) -> EF(s = F ∧ y1 = F ∧ y2 = F ∧ pc10 = T ∧ pc11 = F ∧ pc20 = T ∧ pc21 = F))
— However this is false (there is a state that has no next as init state; init +guard pc2=10)
AG ((s = F ∧ y1 = F) -> EX(s = F ∧ y1 = F ∧ y2 = F ∧ pc10 = T ∧ pc11 = F ∧ pc20 = T ∧ pc21 = F))
— But this can be true: (why?)
AG ((s = F ∧ y1 = F ∧ pc20 = T ∧ pc21 = T) -> EX(s = F ∧ y1 = F ∧ y2 = F ∧ pc10 = T ∧ pc11 = F ∧ pc20 = T∧ pc21 = F))