A PVS-Simulink Integrated Environment for Model-Based Analysis of Cyber-Physical Systems