Simulink　is　an　industrial　de-facto　standard　for　building　executable　models　of　embedded　systems　and　their　environments,　facilitating　validation　by　simulation.　Due　to　the　inherent　incompleteness　of　this　form　of　system　validation,　complementing　simulation　by　formal　verification　would　be　desirable.　A　prerequisite　for　such　an　approach　is　a　formal　semantics　of　Simulink＇s　graphical　models.　In　this　paper,　we　show　how　to　encode　Simulink　diagrams　into　Hybrid　CSP　(HCSP),　a　formal　modelling　language　encoding　hybrid　system　dynamics　by　means　of　an　extension　of　CSP.　The　translation　from　Simulink　to　HCSP　is　fully　automatic.　We　furthermore　discuss　how　to　utilize　a　Hybrid　Hoare　Logic　Prover　to　verify　the　translated　HCSP　models.　We　demonstrate　our　approach　on　a　combined　scenario　originating　from　the　Chinese　High-speed　Train　Control　System　at　Level　3　(CTCS-3).　©　2013　IEEE.