Le but de ce projet, financé par BT, situé à la ETH et co-supervisé par le LRI est d'utiliser de politiques de sécurité comme spécifications et de générer des données de test de manière automatique. Les politiques sont spécifiées en logique d'ordre supérieure (HOL), importées dans le système HOL-TestGen, qui possède un genérateur de tests basé sur un système de preuve programmé. A présent, on cherche à appliquer une méthodologie de modélisation (utilisée dans plusieurs études de cas substantielles) sur le système d'accès aux données des patients dans le "National Program for IT in the NHS England".
Les partenaires sont la ETH Zürich et British Telecom.