Ante el requerimiento de unificar sistemas de información preexistentes, las ontologías se presentan frecuentemente como la mejor opción para resolver interoperabilidad semántica e integrar modelos de datos de fuentes heterogéneas. Entre los lenguajes más populares para especificar dichas ontologías se encuentra OWL, un lenguaje basado en lógica descriptiva y soportado por un razonador que permite chequear la consistencia lógica. Sin embargo, tiene ciertas limitaciones para verificar y validar algunos aspectos relevantes. Por ejemplo, carece de características que posibiliten chequear si la ontología es coherente con el dominio del conocimiento, si es compatible para recuperar la información deseada, o si es completa y consistente de acuerdo a los requerimientos. Alloy es un lenguaje formal soportado por un analizador automático SAT, que habilita la Verificación y Validación (V&V) de modelos.
La presente línea de investigación tiene como objetivo estudiar el uso de Alloy para la V&V de ontologías en OWL desarrolladas para unificar modelos de datos heterogéneos. Como caso de estudio se plantea la V&V con Alloy, de una ontología genérica a nivel nacional especificada para unificar el modelo de datos utilizado en de las distintas jurisdicciones dentro los sistemas de información de los Poderes Judiciales de Argentina.