随着软件系统的日益庞大,对软件的要求也越来越高,对软件模型的验证和性能的度量,受到前所未有的关注,同时基于统一建模语言(Unified Modeling Language, UML)[1][2]的软件设计方法也日益成为一种行业标准,因此从UML中获得一些需求和性能的信息,分析并发现系统中潜在的漏洞和性能瓶颈,将成为一种优秀的解决方法。UML是一种通用的可视化建模语言,它具有建模方法直观、易于理解、便于表达和使用、代码生成等优点。但是UML语言缺少精确的形式化描述。而Petri网则是一个侧重描述动态行为的形式化描述语言,尤其能很好的描述系统的并发和分布系统[3]。本文充分结合UML和Petri网这两种建模语言,互相取长补短:一方面可以对软件进行直观设计,另一方面可以描述软件的动态行为。首先将系统用UML进行描述,然后把带有非功能信息的UML状态图转换为Petri网模型,基于这个Petri网模型,我们可以验证功能性和对非功能性进行度量。在功能性验证方面,过滤Petri网模型中的非功能信息,通过定义转换规则将Petri网转到模型检测工具SPIN的输入语言—PROMELA语言,我们将所要检查的功能用线性时序逻辑公式(LTL)表示。通过分析SPIN的运行结果和系统的执行路径,我们可以判断出该功能是否满足系统。在非功能度量方面,我们将Petri网转化为随机Petri网(SPN),由于任何含有有穷个库所、有穷个变迁的连续时间的SPN同构于一个连续时间马尔可夫链[4]。在马尔科夫链模型的基础上,得出表示系统非功能性质的数学表达式,从而实现对系统可行性、安全性、性能效率等非功能性进行度量。最后文中运用Service Robot例子验证我们的方法。