Visual specifications of policies and their verification

The specification of policies is a crucial aspect in the development of complex systems, since policies control the system's behavior. In order to predict a possibly incorrect behavior of the system, it is necessary to have a precise specification of the policy, better if described in an intuitive formalism. We propose policy specifications in three modeling notations, viz. UML, Alloy and Graph Transformations, and compare them from the viewpoint of readability, verifiability as well as tool support. We use a role-based access control policy as example policy.