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

Claim 5:
6. The method for automatic translation of ladder logic to a SMT-based model checker in a network according to claim 5, wherein said program is a Rockwell L5X file format,
wherein said comparators and arithmetic operators of said program have the notation ADD(a,b,c) for said Addition, SUB(a,b,c) for said Subtraction, MUL(a,b,c) for said Multiplication, DIV(a,b,c) for said Division, MOD(a,b,c) for said Modulo, NEG(a,b) for said Negate, ABS(a,b) for said Absolute value, LIM(−10,a,10) for said Limit, EQU(a,b) for said Equal to, LES(a,b) for said Less than, GRT(a,b) for said Greater than, LEQ(a,b) for said Less than or equal to and GEQ(a,b) for said Greater than or equal to, and
wherein said predefined model functions are matched with said corresponding comparators and arithmetic operators following the construction c=ctx.mk_add(a, b) for said Addition, c=ctx.mk_sub(a, b) for said Subtraction, c=ctx.mk_mul(a, b) for said Multiplication, c=ctx.mk_div(a, b) for said Division, c=ctx.mk_mod(a, b) for said Modulo, b=ctx.mk_minus(a) for said Negate, b=ctx.mk_ite(ctx.mk_lt(a, ctx.mkNumber(“0”, it)), ctx.mk_minus(a), a) for said Absolute value, ctx.mk_and(ctx.mk_geq(a, ctx.mkNumber(“−10”, it)), ctx.mk_leq(a, ctx.mkNumber(“10”, it))) for said Limit, ctx.mk_eq(a, b) for said Equal to, ctx.mk_lt(a, b) for said Less than, ctx.mk_gt(a, b) for said Greater than, ctx.mk_leq(a, b) for said Less than or equal to and ctx.mk_geq(a, b) for said Greater than or equal to.