Integrating object-oriented methods and formal methods for requirement engineering

High quality software requirement specification is crucial for a software development. Although much efforts and research works are done to address the problem, the errors in user requirement are still prevent us from developing high quality software. To address the problem, this paper proposes integrating graphical specification technique UML with formal specification technique to construct user requirement specification. A prototype tool to perform the automatic translation from UML specification into Object-Z specification is presented.