Abstract: Precise formal software specifications are foundation of software description、development and verification, while industrial community in general use non-(semi-) formal representation to define and describe user requirements. It is one of the difficulties of current requirement engineering that how non-(semi-) formal user requirements are generated into the formal software specifications. In this paper, problem pattern is defined by extending the concept of design pattern, then a generation approach of formal software specification is proposed based on problem patterns. From the high-level problem requirements described by structured natural language-SNL, they are refined step by step to get various new sub-problem formal specifications by selecting problem patterns from knowledge base. Afterwards the sub problems are composed and optimized to get the final formal specification. Furthermore we use the principle and concepts of model refinement calculus to provide theory basis of the generation method. We adopt algorithmic program domain as research object and use Radl as formal specification language. This approach is elaborated using a classic example about algorithmic program domain, and practical effects manifest that it can effective generate formal specification of high quality.