Abstract: As a case study of hybrid system, a redundancy management system in flight control system is formally investigated and its specification and verification are presented using an approach incorporating program logic into duration calculi. Firstly, the requirement with some assumptions is captured in duration calculi, then the algorithm is specified in mixed-term hybrid descriptions and a parameter selection is given. During the verification phase,the program invariant is reasoned about with Hoare logic and specified by duration formulae. Finally, the whole verification is finished in the duration calculus framework.