Veri¯cation and testing are the important step for software
assurance. However, such crucial and yet challenging tasks
have not been widely adopted in building access control sys-
tems. In this paper we propose a methodology to sup-
port automatic analysis and conformance testing for ac-
cess control systems, integrating those features to Assur-
ance Management Framework (AMF). Our methodology at-
tempts to verify formal speci¯cations of a role-based access
control model and corresponding policies with selected se-
curity properties. Also, we systematically articulate testing
cases from formal speci¯cations and validate conformance
to the system design and implementation using those cases.
In addition, we demonstrate feasibility and e®ectiveness of
our methodology using SAT and Alloy toolset.