Soy nuevo en el campo de los Métodos Formales, pero siento que tengo una comprensión educada de sus aplicaciones. Sin embargo, parece que solo encuentro métodos formales aplicados al proceso de desarrollo, a medida que se crea el software.
Me gustaría poder aplicar métodos formales en el software existente para comprobar si cumple con los controles de acceso basados en roles (RBAC) y la separación de información confidencial siguiendo el método de Bell-LaPadula (BLP).
¿Qué métodos y herramientas conoce que ofrecen una solución automatizada para la verificación similar a RBAC y BLP del software / código fuente existente?