随着软件开发技术和开发平台的不断发展，面向对象的软件设计技术和实现技术已经成为主流。新产生的编程语言也无一不是面向对象的。在面向对象理论的支持下，出现了许多软件快速开发环境和CASE工具，产生了许多新的软件开发过程模型，极大地增加了软件开发的效率。软件设计是软件开发的核心阶段，软件模型的建立之后的验证和精化将直接影响软件的质量。UML作为一种完全支持面向对象的建模语言，提供了从软件开发过程模型，软件模型建立、模型精化、流程分析到软件生成的能力，但是UML缺乏明确的形式语义基础，对UML建立的软件模型的验证不能利用已有的数学工具，只能通过比较需求、评审原型等方式完成，因此，软件模型的精化只能依靠多次重复完成，致使软件成本放大；同时，这样的软件开发过程还不能适应关键系统在可靠性上的要求。 另外一个方面，很多学者也致力于将整个软件开发过程采用数学方法和工具来严格定义，各阶段建立的模型都是从前一个阶段推导产生，并且可以进行证明。人们广泛采用数理逻辑、进程代数等数学工具并发展出时序逻辑、时段演算、Petri网等新的方法，并产生了一些形式化语言如Z、VDM、CSP等。但是这些方法都存在局限性，而主要缺点是对形式化方法的数学特点对程序员来说是一种挑战；形式化语言不能很好的支持面向对象开发；数理逻辑和进程代数等数学方法又不能很好地描述时序、交互、容错；一般来说形式化语言没有好的代码生成系统。 针对以上问题，作者将采用将面向对象软件开发中广泛适用的UML开发过程与具有面向对象特征的RAISE形式化方法结合起来，提出一种新的软件开发方法FDOOM(Pormal Development based on Object Oriented Modeling)，既保留现有面向对象软件开发的优点——可视化，同时能为面向对象方法建立较为严格的规范描述能力，并能够形式化地对软件模型的精化过程进行验证或证明，提高面向对象开发关键软件的可靠性，并在一定程度上减少关键软件需求分析和模型精化的周期。这将对推广形式化方法和最终实现形式化方法的可视化具有积极的意义。 为了实现以上的目标，作者首先研究RAISE的模型表示和模型精化能力，通过寻找RAISE模型和UML的对象模型之间的联系，建立RAISE模型和UML模型之间的“桥梁”，完成使用RAISE的RSL语言表示UML的对象模型。同时根据RAISE的特点，将RAISE开发方法结合到UML的开发过程中，最后提出可视化和形式化初步结合的FDOOM开发方法。 为面向对象建模概念建立语义基础是十分重要的，通过形式化的抽象定义，可建立精确的面向对象的结构模型和行为模型，因此作者将使用RAISE的定义语言RSL来表达UML的类结构，找到UML对象模型和RAISE形式化模型的对应关系。 利用UML的可视化的优点，进行基本的需求分析和建模，然后利用RAISE精确定义模型并进行精化和验证，对己经验证的模型再采用UML重新表示这种新的模型，最后完成软件设计，同时可以利用支持UML的 CASE具 RaionalRose、MS Msio等直接产生代码，产生演化型原型。 为了验证这样的开发过程，本文还将描述港口船舶停靠管理的例子，概要地体现将UML建模和RAISE形式精化模型结合的开发方法。