Automatic support for formal specification construction using pattern knowledge

Although formal specification is considered as a potential technique for improving the accuracy of requirements documentation and the quality of software product, the difficulty of using formal notations leads to the gap between this technique and the practice of software development. Many approaches for solving this problem were proposed. Most of them provide automatic transformation from informal requirements into formal specifications. However, rather than clarifying and formalizing requirements on the semantic level, they only use syntactic rules to translate between different languages. To handle the challenge, this paper describes an approach for formal specification construction based on pattern knowledge. The knowledge is composed of a set of inter-related specification patterns. Each pattern defines the method for formalizing one kind of function, including derivation knowledge for guiding the clarification of the function and transformation knowledge for formally representing the clarified function. A supporting tool is also described in the paper which derives necessary function details of the intended requirement through interactions by applying the derivation knowledge and transforms these details into formal specifications by applying the transformation knowledge. An experiment on the tool is held and the result shows that the tool can help formalize requirements efficiently and enhance the quality of the resultant formal specifications.