随着Web系统的迅猛发展和广泛应用,其功能验证和性能提高越来越受到重视,Web系统的开发成为一项复杂而艰巨的工作。开发者希望在早期就能对系统的功能和性能进行评价,尽早发现设计中存在的缺陷,采取改进措施以提高Web系统的性能。因此,对Web系统进行建模分析和性能评价十分重要。很多学者致力于Web系统建模和仿真的研究,提出了很多形式化建模和性能分析方法,主要有排队网络(Queuing Network)、随机Petri网(Stochastic Petri Net,SPN)、随机进程代数(Stochastic Process Algebra, SPA)、着色Petri网(Colored Petri Net, CPN)等。SPA、SPN和排队网络的求解过程,都是利用对应的马尔可夫链,由于“状态空间爆炸问题”,一个很小的系统转换为数学分析模型都是相当困难甚至是不可能的。SPN具有更强的模型描述能力,尤其对于分布式系统、并行系统和同步系统等的性能分析更是如此,但是随着位置、变迁和token数的增多,仍存在着状态空间爆炸的问题。着色Petri网是一种图形化的系统建模和分析工具,它特别适合描述顺序、并发、冲突以及同步等现象。着色Petri网不仅可以刻画系统的静态结构,还可以分析系统的动态行为。它既有直观的图形表示,又有深刻的数学基础,可以利用马尔可夫链等多种数学工具对模型进行验证和分析。本文考虑用高级Petri网——赋时着色Petri网(TCPN)来建立更加精确的TCPN模型,TCPN更容易描述和分析基于时间的模型中并发处理之间的同步、通信和资源共享等,正适合模拟和分析复杂的Web系统。本文主要工作集中于Web系统流程的改进、TCPN建模和TCPN模型的性能评价,主要工作概括如下:第一,分析了经典Petri网的特点,深入学习了层次着色Petri网,分析了赋时着色Petri网的动态属性和建模优势,学习了CPN Tools的性能分析方法。第二,从理论角度分析了Web系统的工作机制和流程,充分利用TCPN适于模拟和处理流程的特点,用TCPN分析了Web系统流程中可能出现的问题以及如何发现和改进。第三,用基于TCPN理论的形式化方法建立了Web系统模型,通过对用户信息注册和请求响应的具体实例进行状态空间功能验证和Monitor性能分析,实现了Web系统流程调整优化,从而提高了系统性能。