【作者】 陈怡海；

【导师】 缪淮扣；

【作者基本信息】 上海大学 ， 控制理论与控制工程， 2007， 博士

【摘要】 随着计算机硬件性能迅速提高和价格的持续下降，计算机系统应用范围不断地扩大，软件系统也日益复杂，研究如何提高软件质量和软件开发效率的工作变得日益重要。UML语言已成为软件工程领域事实上的标准建模语言，它提供了丰富的建模机制，并且容易让用户理解，因此在抽取和定义用户需求阶段获得了广泛的应用。但由于UML语言缺乏精确的语义，而使得分析设计人员难以建立精确的需求模型，更难以使用工具对模型自动进行系统的分析和验证。形式方法则是一种基于数学的软件开发方法，形式方法能对系统应该满足的性质进行描述，它具有精确性，一致性和无歧义性等特点，并且能够对规格说明进行分析和验证，因此被认为是提高软件质量的有效方法。然而，在工业界，形式方法大都仅用于安全攸关领域。形式方法被批评为难以使用，费时费力，由于需要分析设计人员具备良好的数学基础和抽象思维能力，因此构建形式规格说明比较困难，并且缺少有效的和完整的工具来支持软件开发人员使用形式方法。在软件的开发过程中怎样才能有效地结合面向对象方法与形式方法则是一个值得研究的课题，本文所做的工作和取得的成果主要体现在以下几个方面：●本文以UML和Object-Z作为建模工具，提出了一种在软件需求阶段结合图形化规格说明和形式方法，以获得精确的软件需求规格说明的方法。本文从整个系统的角度研究了如何实现从用户需求得到图形化规格说明，再到形式规格说明，并对规格说明进行有效确认的方法和技术。●在对图形化规格说明技术与形式方法进行对比分析的基础上，指出了它们的优缺点。通过分析得出了这样的结论：将图形化规格说明与形式方法结合，就能互相弥补双方的缺陷和不足，并能最大限度地发挥出各自的优势。同时本文提出了一种结合图形化方法与形式化方法来构造软件需求规格说明的过程。●在UML与形式方法的结合过程中发挥了补充法和结合法的综合优势，首先根据补充法的原则使用OCL对模型信息进行较为精确的描述，再使用结合法，即通过将带OCL约束信息的UML模型转换为Object-Z规格说明使UML模型形式化。使用Object-Z就可以方便地表达面向对象的概念。在总结现有研究成果的基础上，通过分析现有研究成果中的不足之处，系统地提出了一整套从UML类图，状态图以及用例图到Object-Z规格说明的转换规则，并用一个电梯系统的实例加以说明。●在结合UML与Object-Z的研究过程中，发现OCL语言与Object-Z语言具有很强的互补性，给出了从OCL表达式系统地转换到Object-Z规格说明的方法。本方法结合了UML／OCL模型直观性与Object-Z语言的严密性优点，可产生更为完全的Object-Z规格说明。为了支持本文提出的方法，又开发了基于XMI的工具UMLFormalizer，初步实现了从UML模型到Object-Z的自动转换。●目前常见Object-Z存储交换格式有基于Latex和基于XML格式两种，本文在对这两种常见存储交换格式进行分析比较的基础上，认为采用XML格式的Object-Z规格说明文件更有利于形式开发工具的集成，并且对现有的Object-Z规格说明的XML描述进行改进，从而完善了其操作部分，使用XML模式定义了一个Object-Z的XML标记格式，给出了该XML结构的具体定义。●在Object-Z规格说明动画技术研究方面，我们提出了一种形式化规格说明的动画模拟技术确认方法，并设计开发出Object-Z规格说明的一个动画模拟系统——OZAnimator，以便帮助用户对形式规格说明进行确认。更多还原

【Abstract】 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.更多还原