Hybrid System is an embedded computing system composed of computers and physical instruments. It allows the inclusion of continuous components in a reactive real-time system. XYZ/E is a temporal logic language based on Manna-Pnueli's Linear Time Temporal Logic. It combines both static and dynamic semantics in a unified framework and supports the whole procedure of stepwise refinement, i.e. from the abstract specifications to executable codes. In this article, the authors first specify and verify hybrid systems with XYZ/E, then introduce the computational model we selected for the hybrid systems and discuss the formal description of hybrid systems in the TLL XYZ/E. Finally the verification methodology in the framework is discussed. Compared with the related work, XYZ/E supports state transitions such that it can specify complex control algorithms in a convenient way.