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.%精确的形式化软件规格说明是软件描述、开发与验证的基础,而工业界普遍使用非(半)形式化的表示定义与描述用户需求,如何由非(半)形式化的用户需求生成形式化软件规格说明是需求工程的难点之一.将设计模式的概念进行扩展,定义了问题模式,提出了一种基于问题模式形式化软件规格说明生成方法.该方法从结构化自然语言SNL描述的高层问题需求出发,通过选择知识库中的问题模式逐步精化得到各个新的子问题对应的形式化规格说明,之后对各个子问题组合并进行优化以得到最终的形式化规格说明.进一步,使用模型精化演算的原理与概念给出了该生成方法的理论基础.采用算法程序领域作为研究对象并使用Radl语言作为形式化规格说明语言.通过算法程序领域中的典型实例对这一方法进行了详细的描述,实际效果表明该方法能有效地生成高质量形式化规格说明.
展开▼
