协作权限动态管理的赋色Petri网模型与验证

Modeling and Verification of Dynamic Management of Cooperative Permission Based on Colored Petri Nets

针对多用户环境中协作权限动态分配与回收,及可靠性验证问题,提出基于活动、角色的协作权限动态管理机制,采用赋色Petri网建立形式化模型并分析.该模型将共享的协作文档和视图空间按照活动序列划分,角色的分配、回收与活动相关联,解决了传统访问控制中授权用户对访问对象具有持久权限的问题.最后,基于状态空间的分析表明,该模型能够实现活动依赖关系,活动角色绑定可达性及协作权限申请中死锁避免等约束条件的验证,能够满足协同设计中变化频繁的协作权限访问控制需求.

Focusing on assurance of activity based dynamic assignment and retrieve of cooperative permission in multi user environ- ment, and its reliability verification, an activity-role based mechanism of cooperative permission dynamic management is proposed in this paper, and CPNs based modeling and analyzing issues are also provided. In this model, the shared cooperative document and view space are divided according to the sequence of interdependent activities, and the cooperative activities are associated with the as- signment and retrieve of role, therefore, the problem of authorized users with persistent permissions to specific object in traditional ac- cess control is solved. In the final, state space based analysis shows that constraint conditions such as dependencies between activities, reachability of activity-role binding, and deadlock prevention in applying for cooperative permission can be verified, and the require- ments of frequent change of cooperative permission are satisfied in the access control of cooperative design system.