- TLA+ es un lenguaje para modelar software a un nivel más alto que el código, y para modelar hardware a un nivel más alto que el nivel de circuitos
- Proporciona un entorno de desarrollo integrado (IDE) para escribir modelos y verificarlos
- La herramienta más usada por los ingenieros es el model checker TLC, y también ofrece un verificador de pruebas
- TLA+ está basado en matemáticas y no se parece a ningún lenguaje de programación
- Para la mayoría de los ingenieros, es más fácil comenzar con PlusCal que con TLA+
- A los modelos de TLA+ normalmente se les llama "especificaciones". En la introducción de abajo se les llama
modelos
PlusCal
- PlusCal es un lenguaje para escribir algoritmos, en particular algoritmos paralelos y distribuidos
- Se usa para escribir algoritmos como código preciso y comprobable, en lugar de pseudocódigo
- Parece un lenguaje de programación simple y ofrece construcciones para expresar concurrencia y no determinismo
- Puede usar fórmulas matemáticas como expresiones, por lo que es muy expresivo
- Los algoritmos de PlusCal se convierten en modelos de TLA+ y pueden verificarse con herramientas de TLA+
- Como parece un lenguaje de programación, es fácil de aprender, pero TLA+ es más adecuado para estructurar modelos complejos
Qué es un modelo
- Las computadoras y las redes siguen leyes físicas continuas, pero es natural modelar su comportamiento como un conjunto de eventos discretos
- No existe un modelo que describa perfectamente un sistema real; un modelo describe algunos aspectos del sistema con un propósito específico
- TLA+ es un lenguaje de modelado basado en estados que representa la ejecución de un sistema como una secuencia de estados
- Un evento se representa como un par de dos estados consecutivos, y a esto se le llama un "paso" (
step)
- Un sistema se modela como un conjunto de acciones que describen todas las ejecuciones posibles
Modelado por encima del nivel de código
- TLA+ se usa para modelar sistemas por encima del nivel de código
- Por ejemplo, el algoritmo de Euclides puede describirse no como código, sino como un procedimiento para calcular el máximo común divisor (GCD)
- Establecer la variable x en M y la y en N
- Restar repetidamente el valor menor del mayor entre x y y
- Repetir hasta que x e y sean iguales, y ese valor es el GCD
- Esta descripción omite detalles como tipos de variables o manejo de excepciones, y expresa solo la idea esencial del algoritmo
- Si uno se enfoca solo en codificar, es difícil encontrar buenos algoritmos → se necesita pensamiento abstracto
- La mayoría de los programadores empiezan a codificar sin un modelo de alto nivel, y eso provoca errores de diseño
- TLA+ es un lenguaje de modelado de alto nivel que permite describir con claridad el comportamiento del código y su forma de operar
- Cuanto más complejo es el sistema, más importante es simplificarlo, y eso se logra no con técnicas de codificación, sino con pensamiento de alto nivel
- En un proyecto industrial, hubo un caso en el que el modelado con TLA+ redujo a una décima parte el tamaño del código de un sistema operativo en tiempo real
- El modelado es efectivo para encontrar errores de diseño con anticipación y es más confiable que hacer pruebas o corregir código
Modelado de sistemas paralelos
- Un sistema paralelo está compuesto por varios componentes (procesos) que operan al mismo tiempo
- Un sistema distribuido tiene procesos separados espacialmente que se comunican mediante mensajes
- TLA+ modela el estado completo del sistema como un estado global
- Según más de 40 años de experiencia, modelar sistemas distribuidos con base en un estado global es lo más útil en términos generales
Máquina de estados (State Machine)
- TLA+ define un conjunto de acciones con los siguientes dos elementos:
- Condición inicial: especifica los posibles estados de inicio
- Relación del siguiente estado: especifica los posibles pasos (pares de estados consecutivos)
- El conjunto de acciones que satisface estas dos condiciones es el modelo
- A este tipo de modelo se le llama máquina de estados (
state machine)
- Una máquina de estados finitos (
finite-state machine) es una máquina de estados con un número finito de estados
- La máquina de Turing es un ejemplo de máquina de estados; en una máquina de Turing determinista, cada estado tiene como máximo un siguiente estado
- Una forma práctica de describir con precisión la semántica de un lenguaje de programación es una semántica operacional que lo convierte en una máquina de estados
- La acción del siguiente estado solo especifica los pasos que pueden ocurrir; no significa que necesariamente deban ocurrir
- Para indicar que un paso debe ocurrir obligatoriamente, hay que agregar una condición de equidad (
fairness property)
- Incluso sin equidad basta para encontrar errores de comisión (
commission), pero no se detectan errores por omisión (omission)
- En la mayoría de los casos hay más errores de comisión, así que los principiantes deberían comenzar escribiendo la condición inicial y la relación del siguiente estado
Verificación de propiedades
- Se escribe un modelo para comprobar si el sistema funciona como se desea
- Con herramientas de TLA+, se puede verificar si el modelo satisface cierta propiedad en todos los comportamientos posibles
- Ejemplo: aunque en el 99% de los estados iniciales el comportamiento termine normalmente, debe verificarse que todos los comportamientos terminen normalmente
- La propiedad más común es la propiedad de invariancia (
invariance property), que siempre debe ser verdadera en todos los estados
- Los modelos con condiciones de equidad también deben verificar propiedades de vivacidad (
liveness property) → por ejemplo, que la ejecución necesariamente termine
- Las propiedades más complejas pueden expresarse como máquinas de estados, y puede verificarse si otra máquina de estados las implementa
- En TLA+, no hay una distinción formal entre máquina de estados y propiedad; ambas se expresan de la misma manera como fórmulas matemáticas
- Que una máquina de estados implemente otra significa que esa fórmula está contenida lógicamente en la otra
- En la práctica, la mayoría de las veces solo se comprueban invariantes y propiedades de vivacidad simples, pero entender conceptos más complejos también ayuda a prevenir errores en el código
El propio lenguaje TLA+
- TLA+ es un lenguaje basado en matemáticas y no se ve como un lenguaje de programación
- Como los programadores están más familiarizados con lenguajes de programación que con expresiones matemáticas, al principio puede parecer difícil
- Pero en realidad, las matemáticas son más expresivas que los lenguajes de programación
- Ejemplo: el GCD puede definirse como el mayor entero positivo que divide a dos números (sin necesidad de explicar el método de cálculo)
- Una definición matemática permite dejar solo lo esencial para el propósito y abstraer detalles de implementación innecesarios
- La procedimentalización no ofrece abstracción; solo oculta código en otro lugar
- PlusCal es adecuado para iniciarse en TLA+, y aun los usuarios expertos prefieren PlusCal para modelos simples
- Pero para pensar matemáticamente y hacer modelado de alto nivel, es importante aprender TLA+ en sí
3 comentarios
https://cacm.acm.org/research/… Lo usan muy bien en AWS.
Programar no es programar
Lo busqué porque lo mencionaban en este artículo.
Yo también lo vi por primera vez en este artículo, así que estuve investigándolo.