Design and Verification of Mechatronic Object-Oriented Models for Industrial Control Systems