La máquina Stream X ( SXM ) es un modelo de computación introducido por Gilbert Laycock en su tesis doctoral de 1993, The Theory and Practice of Specification Based Software Testing . [1] Basado en la máquina X de Samuel Eilenberg , una máquina de estado finito extendida para procesar datos del tipo X , [2] la Stream X-Machine es un tipo de máquina X para procesar un tipo de datos de memoria Mem con flujos de entrada y salida asociados In * y Out *, es decir, donde X = Out * ×Memoria × Entrada *. Las transiciones de una 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, a partir de 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 prueba funcional completa , [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 la biología computacional , las pruebas de software y la 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 dato 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 está 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 dato fundamental.
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 de memoria actual. Si (como máximo) una transición está habilitada 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. Por lo tanto, cada ruta reconocida a través de la máquina genera una lista φ 1 ... φ n de funciones, y el SXM compone estas funciones juntas para generar una relación sobre el tipo de datos fundamental |φ 1 ... φ n |: X → X .
Stream X-Machine es una variante de X-machine en la que el tipo de datos fundamental X = Out * × Mem × In *. En la máquina X original , los φ i son relaciones generales en 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.