访问控制通过对用户访问系统资源进行安全控制来保护系统资源。基于角色的访问控制模型适合对各种访问控制需求进行建模而且能够简化访问控制管理，基于角色的访问控制模型作为一种授权模型已经广泛用于商业应用系统。由于访问控制模型及其扩展模型有许多约束，而这些约束由于相互影响可能会产生冲突，因此通过验证访问控制模型来避免访问控制漏洞具有重要作用。传统的访问控制模型验证方法针对独立的访问控制模型，能够发现访问控制模型内部不同约束之间的可能潜在冲突。但是传统模型验证方法没有考虑实际系统，由于访问控制系统的安全不仅与访问控制模型有关，还与系统的授权约束相关。因此，对访问控制系统的授权约束进行安全性验证具有重要意义。针对上述问题，本文提出一种基于角色访问控制系统的安全授权验证方法。首先，利用形式化规范语言来描述访问控制系统及其授权约束，包括用统一建模语言(Unified Modeling Language,UML)类图表示访问控制模型，用对象约束语言（Object Constraint Language,OCL）描述访问控制系统的授权约束；然后，利用模型驱动架构实现UML模型到形式化模型的转换；最后，利用形式化验证方法对系统的授权约束进行安全性验证。本文最后选取一个基于角色访问控制系统进行实例验证，实验表明针对基于角色访问控制系统的授权约束，该方法能够进行有效的安全性验证。