Controller Verification and Design with Logical Analysis Support