基于角色访问控制（RBAC）模型是一种在信息系统中广泛使用以控制资源访问权限的技术。它允许通过用户的角色而非直接分配给用户的权限来进行访问控制。在RBAC模型中，用户通过指派给他们的角色获取权限，角色之间可以有继承关系，而权限则是与角色关联的操作集合。
本文的作者张昊、孙建华和陈浩，提出了对RBAC模型中安全约束进行验证的一种新方法。该方法的核心在于将RBAC模型中的元素转换为统一建模语言（UML）类图，并采用形式化语言来描述这些模型中的约束。随后，该方法利用模型转换工具将类图及其约束语句转换为形式化验证器能够处理的输入模型。最终，通过形式化验证器结合授权属性对RBAC模型中的约束进行安全性验证。这一系列过程的目的是为了确保在软件设计阶段，能够有效理解和验证安全模型及其相关约束，从而保证软件系统的安全性。
在软件工程领域，UML是一种用来设计和分析面向对象软件系统的标准建模语言。UML提供了丰富的描述方法，可以表述系统的静态结构、动态行为以及各种属性。Shin等人通过使用UML类图来描述RBAC模型，证明了UML在表示RBAC模型方面的可行性。然而，尽管UML类图能够简洁直观地展现RBAC模型，但其在表达RBAC模型中的约束时，并不能做到细致和严谨。因此，作者引入了对象约束语言（OCL），这是一种形式化规范语言，常用于在UML模型中描述各种约束。通过在UML模型中使用OCL语言来表示RBAC模型约束，作者解决了UML类图在描述约束方面的不足。
文章中还提到了引言部分，强调了RBAC模型的形式化分析和验证的重要性，指出这是访问控制研究领域中的重点。由于RBAC模型使用形式化方法来描述，软件开发者直接以形式化安全模型作为开发任务时会遇到困难，因此在软件设计阶段需要一种有效的方法来帮助开发者理解、验证和实施安全模型及其相关约束。
文章提到，通过实验验证了提出的方法能够有效分析和验证RBAC模型约束的安全性。实验结果证明，该方法在实际应用中能够有效地对RBAC模型约束进行安全性验证。
关键词中提到的网络安全、UML、OCL以及约束，均是与该论文研究内容密切相关的术语。网络安全涉及到保护计算机网络系统免受攻击和损害；UML是一种用于软件工程中，用于可视化系统设计的建模语言；OCL则是一种能够对UML模型中概念进行详细和准确描述的语言；约束是指在系统设计和实施过程中为了保持系统安全稳定而必须遵守的规则和限制。
此外，文中还提到了基金项目信息，指出该研究得到了国家自然科学基金的支持，具体的项目编号为***。作者简介方面提到张昊是一位主要研究方向为网络安全的硕士研究生，孙建华是一位副教授，主要研究方向包括网络安全和入侵检测。这些信息提供了研究者的基本背景和研究方向，有助于了解文章的研究背景和作者的专业领域。
