摘要 : A policy is an execution rule (or constraint) for objects in a system to retain security and integrity of the system. We introduce a simple policy specification language and define its operational semantics. A new NFA construction... 展开 A policy is an execution rule (or constraint) for objects in a system to retain security and integrity of the system. We introduce a simple policy specification language and define its operational semantics. A new NFA construction algorithm that works in linear time is proposed and a model checking method for policy controlled system (PCS) is presented. We conducted verification of a sample PCS for hotel reservation by our automatic verification tool and the experimental results showed the efficiency of the proposed method. 收起