Patent ID: 11906943
Assignee: NOZOMI NETWORKS SAGL
Field: Control (Instruments)
Classification: CPC G  H  Y | IPC G

Claim 7:
8. The method for automatic translation of ladder logic to a SMT-based model checker in a network according to claim 7, wherein said program is a Rockwell L5X file format,
wherein said contacts of said program comprise the notation XIC(x) to examine if said switch is closed, which propagates 1 only if the value on the left is 1 and x is 1, and XIO(x) to examine if said switch is open, which propagates 1 only if the value on the left is 1 and x is 0,
wherein said first contacts translating procedure matches with said notation XIC(x) following the construction
Procedure TranslateXIC(element)
if element “is not input”:
 element=var2current[element]
return element,

wherein said second contacts translating procedure matches with said notation XIO(x) following the construction
Procedure TranslateXIO(element)
if element “is not input”:
 element=var2current[element]
return ctx.mk_not(element), and

wherein said coils of said program comprise the notation OTE(y) to energy output, which assigns 1 to y if the value on the left is 1 otherwise 0, OTL(y) to latch output, which assigns 1 to y if the value on the left is 1 otherwise leave unchanged, and OTU(y) to unlatch output, which assigns 0 to y if the value on the left is 1 otherwise leave unchanged, wherein said first coils translating procedure matches with said notation OTE(y) following the construction
Procedure TranslateOTE(element)
var2current[element]=element2precondition[element]
return var2current[element]

wherein said second coils translating procedure matches with said notation OTL(y) following the construction
Procedure TranslateOTL(element)
var2current[element]=ctx.mk_or(var2current[element], element2precondition[element])
return var2current[element], and

wherein said third coils translating procedure matches with said notation OTU(y) following the construction
Procedure TranslateOTU(element)
var2current[element]=ctx.mk_and(ctx.mk_not(element2precondition[element]),
 var2current[element])

return var2current[element].