基于SPIN的CSCW系统的验证  

Using SPIN to Validate CSCW System

作　　者：单卓为 鱼滨[2] 

机构地区：[1]西北大学信息学院计算机系,陕西西安710127 [2]西安电子科技大学计算机学院,陕西西安710071

出　　处：《计算机技术与发展》2008年第4期9-12,15,共5页Computer Technology and Development

基　　金：国家自然科学基金重点项目(60433010)

摘　　要：近年来,CSCW系统呈现出用户越来越多、权限关系越来越复杂、组织结构规模越来越大、处理的情况越来越复杂的趋势。因此,CSCW系统的访问控制策略以及访问控制策略的验证已成为国内外CSCW领域十分值得研究和探讨的问题。针对CSCW系统设计的特点,提出了一种验证策略。结合具体实例,使用RBAC模型描述CSCW系统的访问控制权限,利用SPIN工具将模型检测应用于验证CSCW系统属性。Recently,CSCW system has shown a development tendency which has more users, more complex permission connection, larger configuration dimension, and more complicated cases to deal with. Consequently, the accessing control policy of CSCW system and the validation of it have become quite study-worthy topics in and out of China. Focusing on the design traits of CSCW system,has proposed one validation tactic of CSCW system. Researchers illustrate this validation tactic with examples, use RBAC model to depict the accessing control permission of CSCW system, and use the SPIN tool to apply modal check to validate the attribute of CSCW system.

关 键 词：CSCW 角色访问控制 时序逻辑 模型检测 SPIN 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]