SOZRSL Software Requirement Specification Language And Refinement

Formal method represents the reasonable direction in software development. The degree of software development automation influences the future of formal methods. And software development automation relies on the degree of software refinement automation.Structured methods, object-oriented methods and formal methods are three kinds of prime software development methods. Based on the analysis of these three kinds of method, this thesis integrates their advantages and proposes a new software development method called SOFM(Structured Object-oriented Formal Method). The core of SOFM is big structure and small object. The main idea of SOFM is that when developing a software system, it utilizes the structured method based on Data Flow Diagram and object-oriented method, and during the whole software development, it adopts a practical way to apply formal method, and then SOFM adopts refinement method to derive the needed software code. To support the SOFM, we propose a new software development language SOZRSL (Structured Object-Z Requirement Specification Language). To implement the idea of integration of structure method + Object-oriented + formal method, SOZRSL adopts Hierarchy Predicate Data Flow diagram (HPDFD) embedded in Object-Z. HPDFD is the improvement and formalization of traditional data flow diagram. To make SOZRSL more accurate and rigorous, we give the rigorous axiom semantic of SOZRSL.One of the advantages of formal methods is that it facilitates software design automation. To transform specification written in SOZRSL into concrete program code automatically, we discuss the refinement of SOZRSL specification in this paper. Here the refinement of SOZRSL specification is divided into structure refinement, data refinement and predicate refinement. In the structure refinement process, we give the method of mapping SOZRSL hierachical structures into concrete program codes; In the data refinement, we give the method and rules of transforming the abstract data type in the specification into more concrete and computer oriented data type which can be supported by concrete language; In the predicate refinement, we discuss the Tableau method, theorem proving based program refinement and introduce extended Tableau based deduction- coalition. We use this rule to give the refinement method for operations AND and OR of SOZRSL schema . Those methods simplify the refinement of schema composition. In order to make Tableau method available to SOZRSL specification refinement, we define the rules that are used to translate the structure of SOZRSL language into the structure, which can be accepted by Tableau method.The improvement of automating refinement asks the rules searched are more applicable. One approach of improving refinement efficiency is improving the searching and matching efficiency of rules. In order to improve the matching efficiency of rules, we firstly apply the genetic algorithm in the rules selection. Genetic algorithm possesses the characteristics of high initial convergence speed. When the solutions are close to theoptimized solutions, the convergence speed of GA becomes low. So, we can use above characteristics of GA to improve refining efficiency. Fist, we apply the GA to the rules searching process to get a set of optimized solutions. Then people guide the refining process to proceed with the help of their knowledge and experience.Finally, we discuss the detailed implementation of SOZRSL refinement system and visual editor support for SOZRSL, Object-Z and Z specification language.