访问控制模型是管理主体对客体访问限制的策略，通过访问控制模型保证只有被授权的用户才能访问相应的系统资源，提升系统数据安全性和完整性。本文主要研究了基于角色的访问控制模型，针对模型局限性提出改进模型，并对改进模型进行形式化描述和可满足性证明，最后通过煤质管理信息系统对模型进行验证。本文在分析访问控制实现机制的基础上，对比了DAC、MAC和RBAC访问控制模型，着重分析了隐藏在RBAC模型中的局限性和缺乏形式化描述的问题，提出了基于角色的访问控制改进模型。从主体集、客体集和权限集三部分进行改进，建立新的访问控制模型，给出系统的权限控制和访问流程，结合系统开发经验列举开发过程中安全策略。针对RBAC模型缺乏形式化描述和可满足性证明的问题，借助基本描述逻辑语言ALC对改进模型进行形式化描述，利用ALC语法和语义，建立描述逻辑知识库K，给出Tbox术语集、Abox断言集和模型的形式化描述概念表达式。最后采用Tableau算法对模型进行可满足性证明，验证了模型合理性。最后，基于Java语言，在Eclipse开发环境上建立JSP+Struts2+Spring+iBatis架构的大型煤炭企业煤质管理信息系统。主要实现系统管理模块，验证模型的权限分配和访问控制过程，进而得出模型可行性和有效性。研究成果应用于某大型煤炭集团的煤质管理信息系统中，结果表明：本文提出的基于角色的访问控制改进模型进行形式化描述之后，概念消除歧义，便于理解和扩展，而且模型可满足系统需求。实际系统开发之后表明模型可以解决RBAC模型的局限性，简化权限配置过程，实现权限的细粒度访问控制，易于被当前主流框架实现，具有使用和推广价值。