访问控制技术是信息系统必不可少的模块,其中基于角色的访问控制模型RBAC是目前主流的访问控制模型。很多研究都集中在对RBAC模型的建立和分析上。但是在模型的建模和形式化分析上仍然存在一定的缺陷。传统的方法是在系统开发后期建立安全模型,使得安全模型与系统需求存在一定的缺口。如果在系统开发早期建立安全模型,能够及早的发现安全问题,预防安全体系的缺口。另一方面的问题主要集中在模型的分析和判断上,形式化后的模型可以使系统开发人员能够有效的理解和分析模型。本文将用例建模和图变换理论应用在角色访问控制模型上,对RBAC模型的建模和形式化问题进行了研究。本文的研究工作集中在以下三个方面:一是提出了用例驱动的角色安全授权。论文利用用例模型的概念和角色访问控制模型的特征,提出了一种通过用例驱动来定义系统模型角色权限的方法。该方法通过扩展的用例以及形式化的顺序图,将用例模型与角色访问控制模型相结合。而且该方法完全符合最小权限原则。二是提出了基于图变换理论的角色访问控制建模及分析方法。文章描述了RBAC模型的图变换规则建模思想,并在此基础上分析了图变换的正确性,通过规则实例给出了其证明过程。三是以开放式实验室管理系统为平台,研究了系统的用例建模和访问控制安全模型。在此基础上对开放式实验室管理系统的访问控制安全模型进行了形式化的分析。这种基于图变换理论的形式化转换方法能够帮助开发人员有效的理解和分析模型。