The Study Of Construction And Validation Of Object-oriented Formal Specification

With the rapid improvement of computer hardware performance and the decline of price, the application area of computer system is extending continuously. While the software system is becoming more and more complicated, research on how to better the software quality and improve the software development efficiency becomes crucial.The unified modeling language (UML) is becoming the defacto modeling language in software engineering field. It provides rich modeling mechanism, and easy for average user to understand, so it is widely used in the user requirement election and definition stages. However lack of formal semantics of UML makes it difficult for system analyst to develop a precise requirement model, therefore it becomes even more difficult to use software tools to automatically analyze, verify and validate the model.Formal method is a software development method based on mathematics. It can formally specify the properties, which the software system should satisfy. It has the characteristic of preciseness, completeness and unambiguousness, which can be used to analyze and validate formal specification It is regarded as one of the promising methods to improve the software development quality. However formal method is mainly used in safety critical area in industry. Formal method is often criticized for its difficult using and time consuming. Since it requires good mathematics background and abstract logical thinking ability of software analyst to use formal method, creating formal specification is hard, and lack of effective and integrated tools prevends software developers from utilizing formal method.It is a worthwhile topic on how to effectively integrate object-oriented software development method and formal method. The research objectives and main contributions in the thesis are listed as follows:This thesis uses UML and Object-Z as modeling tool and proposes a method to integrate graphical specification technique and formal method, which aims to get precise software requirement specification. The thesis researches how to get the graphics specification from user requirement and how to derive the corresponding formal specification and the approaches to effectively validate and verify the formal specification from the system perspective.Based on the analysis of the graphics specification technique and formal method, it points out the advantages and disadvantages. From careful analysis the conclusion is: the integration of graphics specification technique and formal methods can complement limitation of each other and fully develop each method's potential. This thesis proposes a development method of integrating graphics method and formal method to constitute software requirement specification.During the process of integrating UML and formal method, complementary method and integration method are synthesized. Firstly OCL(Object Constraint Language) is used to give more precise description of the UML model by utilizing complementary method, then integration method is used, i.e. translating the UML model incorporating OCL constraints to Object-Z specification, to formalize UML models. By using Object-Z specification language, Object-oriented concepts can be easily expressed. Based on the existing results and analysis the shortcoming of current researches, this thesis systematically proposes a full set of translation rules from UML class diagrams, state-chart diagrams and use-case diagrams to Object-Z specification. An elevator system example is given to illustrate the approach.During the research process of integrating UML and Object-Z, the OCL and Object-Z language are found to be complementary to each other and an approach to systemically translate OCL expression into formal Object-Z notation is proposed. The approach combines the merits of the intuition of UML/OCL models and the preciseness of Object-Z specification language, which can be used to generate more complete Object-Z specification. In order to support the proposed approach in this thesis, a XMI based prototype tool named UML Formalizer is developed to realize the automatic translation from UML model into Object-Z specification.Based on the analysis of current frequently used Object-Z exchange formats, Latex and XML format, this thesis compares and analyzes both exchange formats and concludes that the XML based Object-Z specification format is more suitable for tool integration. The thesis improves existing XML mark-up format of Object-Z specification language and particularly consummates the operational parts and utilizes XML schema to define the XML mark-up format of Object-Z specification language. A detailed definition of the XML structure is given.In the research area of Object-Z specification animation, this thesis proposes a validation method to animate formal specification and develops a prototype tool: OZAniamtor, to animate Object-Z specification, which can help users to validate formal specification.