Lógica Temporal en Verificación de Modelos de Software: origen y evolución hasta tiempos actuales

In critical software systems, such as control systems for aircrafts or elevators, software errors should be avoided. Nowadays, there exist techniques and tools for ensuring correctness in critical systems, being �model checking� one of the most popular. With model checking, software systems and desired system properties (security, reachability, etc.) are modeled using formal specification languages, i.e. specification languages based on logical-mathematic concepts. Properties are often specified using a type of logic called �temporal logic�. Going into such logic, the present work shows the related epistemological features, detailing the origin and evolution of temporal logic from the first concepts about logics introduced by Aristotle to its conception as a key tool for verifying critical software systems.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