Elevators are crucial for modern buildings, transporting large volumes of passengers across multiple floors every day. Among their components, the scheduling control system plays a central role in determining passenger wait times and overall efficiency. However, traditional simulation-based testing is time-consuming and costly, which limits its scalability. We present an approach that combines both verification and testing for elevator scheduling systems. Our technique models the scheduling logic as a state machine and translates it into Satisfiability Modulo Theories (SMT) formulas that can be efficiently solved and tested by SMT solvers. Preliminary evaluation shows that our technique can verify key properties of scheduling control logic. Our experimental results demonstrate that the approach scales reasonably well with increasing numbers of floors and requests. This can provide a potential practical and automated verification solution for industrial elevator controllers.