La máquina Stream X ( SXM ) es un modelo de cálculo presentado por Gilbert Laycock en su tesis doctoral de 1993, La teoría y práctica de las pruebas de software basadas en especificaciones . [1] Basado en Samuel Eilenberg 's X-máquina , una extendida máquina de estado finito para el procesamiento de datos del tipo X , [2] la Corriente X-máquina es un tipo de X-máquina para el procesamiento de un tipo de datos de memoria Mem con flujos de entrada y salida asociados In * y Out *, es decir, donde X = Out * ×Mem × In *. Las transiciones de un Stream X-Machine están etiquetadas por funciones de la forma φ: Mem × In → Out × Mem , es decir, que calculan un valor de salida y actualizan la memoria, desde la memoria actual y un valor de entrada.
Aunque la máquina X general había sido identificada en la década de 1980 como un modelo formal potencialmente útil para especificar sistemas de software, [3] no fue hasta la aparición de Stream X-Machine que esta idea pudo explotarse por completo. Florentin Ipate y Mike Holcombe desarrollaron una teoría de pruebas funcionales completas , [4] en la que los sistemas de software complejos con cientos de miles de estados y millones de transiciones podrían descomponerse en SXM separados que podrían probarse exhaustivamente, con una prueba garantizada. de correcta integración. [5]
Debido a la interpretación intuitiva de Stream X-Machines como "agentes de procesamiento con entradas y salidas", han atraído un interés creciente, debido a su utilidad para modelar fenómenos del mundo real. El modelo SXM tiene aplicaciones importantes en campos tan diversos como biología computacional , pruebas de software y economía computacional basada en agentes .
Una Stream X-Machine (SXM) es una máquina de estado finito extendida con memoria auxiliar, entradas y salidas. Es una variante de la máquina X general , en la que el tipo de datos fundamental X = Out * × Mem × In *, es decir, una tupla que consta de un flujo de salida, la memoria y un flujo de entrada. Un SXM separa el flujo de control de un sistema del procesamiento realizado por el sistema. El control es modelado por una máquina de estados finitos (conocida como el autómata asociado ) cuyas transiciones están etiquetadas con funciones de procesamiento elegidas de un conjunto Φ (conocido como el tipo de la máquina), que actúan sobre el tipo de datos fundamentales.
Cada función de procesamiento en Φ es una función parcial, y se puede considerar que tiene el tipo φ: Mem × In → Out × Mem , donde Mem es el tipo de memoria e In y Out son respectivamente los tipos de entrada y salida. En cualquier estado dado, se habilita una transición si el dominio de la función asociada φ i incluye el siguiente valor de entrada y el estado actual de la memoria. Si (como máximo) se habilita una transición en un estado dado, la máquina es determinista . Cruzar una transición equivale a aplicar la función asociada φ i, que consume una entrada, posiblemente modifica la memoria y produce una salida. Cada trayectoria reconocida a través de la máquina, por lo tanto genera una lista φ 1 ... φ n de funciones, y la SXM compone estas funciones juntos para generar una relación del tipo de datos fundamental | φ 1 ... φ n |: X → X .
El Stream X-Machine es una variante de X-machine en el que el tipo de datos fundamental X = Out * × Mem × In *. En la máquina X original , φ i son relaciones generales sobre X. En Stream X-Machine, estos suelen estar restringidos a funciones ; sin embargo, el SXM solo es determinista si (como máximo) se habilita una transición en cada estado.