Verification of Behavioral Substitutability in Object-oriented Models for Industrial Controllers