Formal verification of PLC programs using the B method