We present an approach to embedding a formal method into Rational Unified Process (RUP). The purposes are: (a) to unify different views of UML. (b) to enhance UML with the formal method to improve the quality of software systems; and (c) to support effective use of the formal method for system specification and reasoning with the iterative and incremental approach by providing a unified conceptual framework. One of the main features of RUP is that it is use-case driven and supports iterative development more explicit than other process models, such as the waterfall model. Object-orientation also supports better and more explicitly incremental programming than the traditional imperative programming. These together will help to scale up the use of the formal method in software system development. The model is based on Hoare and He's Unifying Theories of Programming (UTP). © 2004 Elsevier B.V. All rights reserved.