Nowadays, the main reason for failures of large-scale systems development is that the requirement analysis stage could not produce complete, understandable, unambiguous, traceable and testable system requirements documents. To conquer this problem, from the point of view of “requirements engineering (RE)”, the formalization of RE process is discussed here from three aspects: a full process model, formal representation and formal verification. RE is taken as a process growing in the 3-demension space of sociology, methodology and technology, and a spiral lifecycle model of this process is given to illustrate its social characteristic. The recommended representation language is UML and Coq is the instrument of Component-Cut-In modularizational formal method to do Validation & Verification. At last, the alternating-bit protocol is an example to demonstrate how to combining UML and Coq to formalize RE.