互联网架构的飞速发展，促进了Web应用的广泛应用。Web应用在国计民生、商业领域和个人生活中发挥着日益重要的作用。现今，Web应用已发展成为一种成熟而又复杂的分布式系统，并且日趋专业化和协作化，针对它的分析、建模及测试工作给软件工程领域带来了极大的挑战。 本文提出一种基于组件的Web应用的建模方法。该方法用于其设计阶段，先将Web应用组件划分为视图组件和服务器端组件，其中视图组件封装Web页面的行为，服务器端组件封装业务逻辑处理，然后给出Web应用的UML组件结构模型和行为模型。该组件模型既提高了Web页面的抽象层次，又统一了Web页面与Web应用后台服务器中组件的描述方式。 UML模型虽然图形表示能力很强，有很好的易用性及可理解性，但其半形式表示方法缺乏精确的语义，产生的规格说明往往不够精确和完整，从而造成系统的不完善。如果提供精确的软件规格说明，将有利于对系统实现的精确描述，使误解引起的错误减少，而软件形式方法正是基于严格精确的数学逻辑模型，可以进行高度抽象的推理与证明过程，并且能够对形式规格说明进行正确性证明。但是形式规格说明中的数学概念抽象，从而导致规格说明难以阅读。由于图形化规格说明和形式方法在软件开发过程中有各自的优缺点，将两者结合起来，则可以产生既容易理解又精确的软件规格说明。 为了提高UML组件模型的精确性，本文采用UML与形式语言Obiect-Z相结合的方法来描述Web应用组件，将结合OCL表达式的Web应用的UML组件模型，转换成Obljeot-Z的形式规格说明。并开发了基于XMI(XML Metadata Interchange)的工具WebMoF，实现了Web应用的UML模型到Obiect-Z形式规格说明的自动转换。