信息科技的发展正在改变着世界，数据库也从最简单的存储数据的表格发展到海量数据存储的大型数据库系统，并在互联网、金融、医疗、电力、电子商务等领域等到了广泛应用。数据库并发控制是数据库事务管理中的重要部分，是衡量一个数据库系统并行性能好坏的重要标志之一。随着互联网技术的发展，对数据库系统的并发度提出了更高的要求，如何在提高数据库并发性能的同时，保证数据的一致性确保数据安全使用，是当前面临的难题之一。　　 本文在深入研究现有的基于有色Petri网(Coloured Petri Net，CPN)的协议分析方法的基础上，针对数据库并发控制协议进行研究，提出了通用的CPN建模分析方法，该方法借助于CPN tools工具，可以对数据库并发协议进行有效的分析。并应用排队论理论对数据库系统进行了性能评价方面的研究。论文主要研究工作及成果如下：　　 1、提出一种基于CPN模型的数据库并发控制协议通用分析方法　　 针对现有方法通用性差的缺陷，在通用认证说明语言CAPSL的基础上提出基于CPN模型的数据库并发控制协议通用形式化描述方法。通过研究数据库并发控制协议的共性，基于CPN的分层思想，增加有利于形式化建模的分层建模概念描述，建立了可通用性强的顶层模型及基础函数库。并且，该分析方法将面向对象语言中的继承派生思想引入到建模当中，即复杂的功能模型可在已有函数库的基础上进行二次建模，提高了经典函数模型的复用性，降低了建模时间成本。　　 2、提出一种基于CPN tools的数据库并发控制协议自动验证分析工具　　 Petri网在数据库并发控制协议方面建立了许多经典模型，但其模型仿真一直停留在理论阶段，缺少简易可靠的仿真平台。本文在CPN tools模型工具的基础上，提出了数据库并发控制协议的自动验证分析工具。该工具将文中提出的协议通用分析方法实体化，并应用状态空间路径法对协议进行死锁检测。大大降低了人工排查的成本，提高了协议问题捕获的准确性。并将工具应用于典型数据库并发控制协议2PL上，体现出较强的可操作性。　　 3、建立一种基于排队论模型的数据库系统性能分析方法　　 基于排队论应的数据库系统瓶颈问题分析中，把数据库系统中的主要部件作为排队网络模型中的节点，建立一个排队网络模型，把排队网路中的理论和方法应用到数据库系统中各部件的瓶颈分析中，为查找数据库系统中的瓶颈提供一种有效的分析方法。　　 本文的解决方案的可用性和有效性都通过具体的实例来证明。结果表明，本文提出的基于CPN的数据库并发控制协议形式化方法具有一定的通用性、基于CPN tools的数据库并发控制协议仿真工具实现了自动验证功能、并结合了排队论理论模型，提出了性能分析形式化的办法，对其他更复杂协议系统的研究均有借鉴意义。