In Special Publication 800-192, it reviews methods for the verification for access control models and the testing of model implementations. SP 800-192 defined structures for AC models, and demonstrated the expressions of AC models and safety requirements in a specification language of a model checker. The document showed the use of black box and white box model checkers that verify the integrity, coverage, and confinement of the specified safety requirements against models. In addition, an efficient way of generating test cases for the implementation from a model as well as a method for detecting AC rule faults in real time are discussed.