This report presents a general method to cope with hybrid control
system specification and verification by making full use of both the
simplicity of finite automata and the excessive expressing power of
Mean Value Duration Calculus. The method consists of four steps:
First, specify the requirements of the whole system through Mean Value
Duration Calculus formulas. Second, use two real-time communicating
automata to characterize the design decisions, which describe the
plant and control subsystems respectively. Third, translate the
automata into Mean Value Duration Calculus formulas. Finally prove the
design decisions conforming to the requirements specification.  Taking
the steam-boiler problem raised by J.-R. Abrial[1] as a running
example, we demonstrate the above method in three versions of
abstractions. Each version represents an abstract level for capturing
the original problem requirements and provides a complete procedure of
applying the above method.  In addition to specifying safety property,
emphasis is put on capturing non-functional requirements such as
performance, reliability, and optimization. Some formal design
techniques about finding an optimal implementation conforming to the
system specification are also discussed.