Resumen:
En sistemas de software críticos, tales como sistemas de control de vuelo de aviones o sistemas de control de ascensores, los errores de software deben ser evitados. En la actualidad, existen técnicas y herramientas para asegurar la correctitud de sistemas críticos, siendo “model checking” (chequeo de modelos) una de las más populares. Con model checking, tanto el sistema de software como las propiedades deseadas del sistema (seguridad, alcanzabilidad, etc.) se modelan utilizando lenguajes de especificación formal; es decir, lenguajes basados en conceptos lógicomatemáticos. Las propiedades son especificadas normalmente a través de un tipo de lógica denominada “lógica temporal”. Profundizando sobre dicha lógica, el presente trabajo muestra los aspectos epistemológicos relacionados, detallando sobre su origen y evolución, desde las nociones de lógicas introducidas por Aristóteles hasta su concepción como herramienta clave para la verificación de sistemas de software críticos.