La máquina X ( XM ) es un modelo teórico de cálculo introducido por Samuel Eilenberg en 1974. [1] La X en "máquina X" representa el tipo de datos fundamentales en el que opera la máquina; por ejemplo, una máquina que opera sobre bases de datos (objetos de tipo base de datos ) sería una máquina de base de datos . El modelo de la máquina X es estructuralmente el mismo que la máquina de estados finitos , excepto que los símbolos utilizados para etiquetar las transiciones de la máquina denotan relaciones de tipo X → X. Cruzar una transición equivale a aplicar la relación que la etiqueta (calcular un conjunto de cambios al tipo de datos X ), y recorrer un camino en la máquina corresponde a aplicar todas las relaciones asociadas, una tras otra.
Teoría original
La máquina X original de Eilenberg era un modelo teórico de computación completamente general (subsumiendo la máquina de Turing , por ejemplo), que admitía cálculos deterministas, no deterministas y sin terminación. Su obra fundamental [1] publicó muchas variantes del modelo básico de la máquina X, cada una de las cuales generalizaba la máquina de estados finitos de una manera ligeramente diferente.
En el modelo más general, una máquina X es esencialmente una "máquina para manipular objetos de tipo X". Suponga que X es un tipo de datos , llamado tipo de datos fundamental , y que Φ es un conjunto de relaciones (parciales) φ: X → X. Una máquina X es una máquina de estados finitos cuyas flechas están etiquetadas por relaciones en Φ. En cualquier estado dado, se pueden habilitar una o más transiciones si el dominio de la relación asociada φ i acepta (un subconjunto de) los valores actuales almacenados en X. En cada ciclo, se supone que se toman todas las transiciones habilitadas. Cada ruta reconocida a través de la máquina genera una lista φ 1 ... φ n de relaciones. Llamamos a la composición φ 1 o ... o φ n de estas relaciones la relación de trayectoria correspondiente a esa trayectoria. El comportamiento de la máquina X se define como la unión de todos los comportamientos calculados por sus relaciones de trayectoria. En general, esto no es determinista, ya que la aplicación de cualquier relación calcula un conjunto de resultados en X. En el modelo formal, todos los resultados posibles se consideran juntos, en paralelo.
A efectos prácticos, una máquina X debería describir algún cálculo finito. Una función de codificación α: Y → X convierte de algún tipo de datos de entrada Y al estado inicial de X, y una función de decodificación β: X → Z, vuelve a convertir desde el estado o estados finales de X a algún tipo de datos de salida Z. Una vez que se completa el estado inicial de X, la máquina X se ejecuta hasta el final y luego se observan las salidas. En general, una máquina puede interbloquearse (bloquearse), o livelock (nunca detenerse), o realizar uno o más cálculos completos. Por esta razón, la investigación más reciente se ha centrado en máquinas X deterministas, cuyo comportamiento se puede controlar y observar con mayor precisión.
Ejemplo
Se puede pensar en un compilador con un optimizador de mirilla como una máquina para optimizar la estructura del programa. En esta máquina Optimizer , la función de codificación α toma el código fuente del tipo de entrada Y (la fuente del programa) y lo carga en el tipo de memoria X (un árbol de análisis). Suponga que la máquina tiene varios estados, llamados FindIncrements , FindSubExprs y Completed . La máquina se inicia en el estado inicial FindIncrements , que está vinculado a otros estados a través de las transiciones:
FindIncrements → DoIncrement FindIncrements FindIncrements → SkipIncrement FindSubExprs FindSubExprs → DoSubExpr FindSubExprs FindSubExprs → SkipSubExpr Completed
La relación DoIncrement mapea un subárbol analizado correspondiente a "x: = x + 1" en el subárbol optimizado "++ x". La relación DoSubExpr mapea un árbol de análisis que contiene múltiples apariciones de la misma expresión "x + y ... x + y" en una versión optimizada con una variable local para almacenar el cálculo repetido "z: = x + y; ... z ... z ". Estas relaciones solo están habilitadas si X contiene los valores de dominio (subárboles) en los que operan. Las relaciones restantes SkipIncrement y SkipSubExpr son nullops (relaciones de identidad) habilitadas en los casos complementarios.
Por lo tanto, la máquina Optimizer se ejecutará hasta su finalización, primero convirtiendo las adiciones triviales en incrementos en el lugar (mientras se encuentra en el estado FindIncrements ), luego pasará al estado FindSubExprs y realizará una serie de eliminaciones de subexpresiones comunes, después de lo cual pasará al estado final Completado . La función de decodificación β se mapeará entonces desde el tipo de memoria X (el árbol de análisis optimizado) al tipo de salida Z (código de máquina optimizado).
Convención
Cuando se hace referencia al modelo original de Eilenberg, "X-machine" se escribe típicamente con una "m" minúscula, porque el sentido es "cualquier máquina para procesar X". Cuando se hace referencia a modelos específicos posteriores, la convención es utilizar una "M" mayúscula como parte del nombre propio de esa variante.
Decenio de 1980
El interés en la máquina X fue revivido a fines de la década de 1980 por Mike Holcombe, [2] quien notó que el modelo era ideal para propósitos de especificación formal de software , porque separa claramente el flujo de control del procesamiento . Siempre que se trabaje a un nivel suficientemente abstracto, los flujos de control en un cálculo generalmente se pueden representar como una máquina de estados finitos, por lo que para completar la especificación de la máquina X todo lo que queda es especificar el procesamiento asociado con cada una de las transiciones de la máquina. La simplicidad estructural del modelo lo hace extremadamente flexible; otras ilustraciones tempranas de la idea incluyeron la especificación de Holcombe de las interfaces humano-computadora, [3] su modelado de procesos en bioquímica celular, [4] y el modelado de Stannett de la toma de decisiones en sistemas de comando militar. [5]
Decenio de 1990
Las máquinas X han recibido una atención renovada desde mediados de la década de 1990, cuando se descubrió que la determinista Stream X-Machine [6] de Gilbert Laycock sirve como base para especificar grandes sistemas de software que son completamente probables. [7] Otra variante, la Communicating Stream X-Machine ofrece un modelo comprobable útil para procesos biológicos [8] y futuros sistemas de satélites basados en enjambres . [9]
2000
Las máquinas X han sido aplicadas a la semántica léxica por Andras Kornai , quien modela el significado de las palabras mediante máquinas "puntiagudas" que tienen un miembro del conjunto base X distinguido. [10] La aplicación a otras ramas de la lingüística, en particular a una reformulación contemporánea de Pāṇini, fue pionera en Gerard Huet y sus colaboradores [11] [12]
Variantes principales
La máquina X rara vez se encuentra en su forma original, pero sustenta varios modelos posteriores de cálculo. El modelo más influyente en las teorías de las pruebas de software ha sido el Stream X-Machine . La NASA ha discutido recientemente el uso de una combinación de Communicating Stream X-Machines y el cálculo de procesos WSCSS en el diseño y prueba de sistemas de satélites de enjambre . [9]
Máquina X analógica (AXM)
La primera variante, la Analog X-Machine de tiempo continuo ( AXM ), fue introducida por Mike Stannett en 1990 como un modelo de computación potencialmente "super-Turing"; [13] se relaciona, en consecuencia, con el trabajo en la teoría de la hipercomputación . [14]
Transmisión de X-Machine (SXM)
La variante de máquina X más comúnmente encontrada es el modelo Stream X-Machine ( SXM ) de Gilbert Laycock de 1993 , [6] que forma la base de la teoría de Mike Holcombe y Florentin Ipate de las pruebas de software completas , que garantiza propiedades de corrección conocidas, una vez finalizadas las pruebas. . [7] [15] El Stream X-Machine difiere del modelo original de Eilenberg, en que el tipo de datos fundamentales X es de la forma Out * × Mem × In *, donde In * es una secuencia de entrada, Out * es una secuencia de salida y Mem es el (resto de) memoria.
La ventaja de este modelo es que permite conducir un sistema, paso a paso, a través de sus estados y transiciones, mientras se observan las salidas en cada paso. Estos son valores testigo, que garantizan que se ejecutaron funciones particulares en cada paso. Como resultado, los sistemas de software complejos pueden descomponerse en una jerarquía de Stream X-Machines, diseñados de arriba hacia abajo y probados de abajo hacia arriba. Este enfoque de dividir y conquistar para el diseño y las pruebas está respaldado por la prueba de integración correcta de Florentin Ipate, [16] que demuestra cómo probar las máquinas en capas de forma independiente es equivalente a probar el sistema compuesto.
Comunicación de X-Machine (CXM)
La primera propuesta para conectar varias máquinas X en paralelo es el modelo de máquina X comunicante ( CXM o COMX ) de Judith Barnard de 1995 , [17] [18] en el que las máquinas se conectan a través de canales de comunicación nombrados (conocidos como puertos ); este modelo existe tanto en variantes discretas como en tiempo real. [19] Las versiones anteriores de este trabajo no eran completamente formales y no mostraban relaciones completas de entrada / salida.
Petros Kefalas desarrolló un enfoque similar de Communicating X-Machine utilizando canales almacenados en búfer. [20] [21] El enfoque de este trabajo fue la expresividad en la composición de componentes. La capacidad de reasignar canales significó que algunos de los teoremas de prueba de Stream X-Machines no se transfirieron.
Estas variantes se analizan con más detalle en una página separada.
Comunicación Stream X-Machine (CSXM)
El primer modelo completamente formal de composición concurrente de máquinas X fue propuesto en 1999 por Cristina Vertan y Horia Georgescu, [22] basado en trabajos anteriores sobre la comunicación de autómatas de Philip Bird y Anthony Cowling. [23] En el modelo de Vertan, las máquinas se comunican indirectamente, a través de una matriz de comunicación compartida (esencialmente una serie de casilleros), en lugar de directamente a través de canales compartidos.
Bălănescu, Cowling, Georgescu, Vertan y otros han estudiado las propiedades formales de este modelo CSXM con cierto detalle. Se pueden mostrar relaciones de entrada / salida completas. La matriz de comunicación establece un protocolo para la comunicación síncrona. La ventaja de esto es que desacopla el procesamiento de cada máquina de su comunicación, lo que permite la prueba por separado de cada comportamiento. Se demostró que este modelo de composición era equivalente a un Stream X-Machine estándar , [24] aprovechando la teoría de pruebas anterior desarrollada por Holcombe e Ipate.
Esta variante de la máquina X se analiza con más detalle en una página separada.
Objeto X-Machine (OXM)
Kirill Bogdanov y Anthony Simons desarrollaron varias variantes de la máquina X para modelar el comportamiento de los objetos en sistemas orientados a objetos. [25] Este modelo difiere del enfoque Stream X-Machine , en que el tipo de datos monolíticos X se distribuye y encapsula en varios objetos, que se componen en serie; y los sistemas son impulsados por invocaciones y devoluciones de métodos, más que por entradas y salidas. El trabajo adicional en esta área se centró en la adaptación de la teoría de las pruebas formales en el contexto de la herencia, que divide el espacio de estado de la superclase en objetos de subclase extendidos. [26]
Simons y Stannett desarrollaron más tarde un modelo de "máquina X aumentada con CCS" (CCSXM) en 2002 para admitir pruebas de comportamiento completas de sistemas orientados a objetos, en presencia de comunicación asincrónica [27]. Se espera que esto tenga alguna similitud con Propuesta reciente de la NASA ; pero aún no se ha realizado una comparación definitiva de los dos modelos.
Ver también
- Transmisión de X-Machine
- Prueba de X-Machine
- Comunicando X-Machine
Informes técnicos descargables
- M. Stannett y AJH Simons (2002) Pruebas de comportamiento completas de sistemas orientados a objetos utilizando máquinas X aumentadas por CCS. Informe técnico CS-02-06, Departamento de Ciencias de la Computación, Universidad de Sheffield. Descargar
- J. Aguado y AJ Cowling (2002) Fundamentos de la teoría de la máquina X para las pruebas. Informe técnico CS-02-06, Departamento de Ciencias de la Computación, Universidad de Sheffield. Descargar
- J. Aguado y AJ Cowling (2002) Sistemas de comunicación X-máquinas para especificar sistemas distribuidos. Informe técnico CS-02-07, Departamento de Ciencias de la Computación, Universidad de Sheffield. Descargar
- M. Stannett (2005) La teoría de las máquinas X - Parte 1. Informe técnico CS-05-09, Departamento de Ciencias de la Computación, Universidad de Sheffield. Descargar
enlaces externos
- http://www.dcs.shef.ac.uk/~ajc/csxms/index.html - Páginas de sistemas de comunicación SXM de Tony Cowling
- http://x-machines.com - Mike Stannett Teoría de la X-Máquinas sitio
Referencias
- ^ a b S. Eilenberg (1974) Autómatas, lenguajes y máquinas, vol. Una . Prensa académica, Londres.
- ^ M. Holcombe (1988) 'Máquinas X como base para la especificación dinámica del sistema', Software Engineering Journal 3 (2), págs. 69-76.
- ^ M. Holcombe (1988) 'Métodos formales en la especificación de la interfaz hombre-máquina', International J. Command and Control, Communications and Info. Sistemas. 2 , págs. 24-34.
- ^ M. Holcombe (1986) 'Modelos matemáticos de bioquímica celular'. Informe técnico CS-86-4, Departamento de Ciencias de la Computación, Universidad de Sheffield.
- ^ M. Stannett (1987) 'Un enfoque organizacional para la toma de decisiones en los sistemas de mando'. Internacional J. Mando y Control, Comunicaciones e Información. Sistemas. 1 , págs. 23-34.
- ^ a b Gilbert Laycock (1993) La teoría y práctica de las pruebas de software basadas en especificaciones . Tesis doctoral, Universidad de Sheffield. Resumen Archivado el 5 de noviembre de 2007 en la Wayback Machine.
- ^ a b M. Holcombe y F. Ipate (1998) Correct Systems - Building a Business Process Solution . Springer, Serie de Computación Aplicada.
- ^ A. Bell y M. Holcombe (1996) 'Modelos computacionales de procesamiento celular', en Computation in Cellular and Molecular Biological Systems , eds. M. Holcombe, R. Paton y R. Cuthbertson, Singapur, World Scientific Press.
- ^ a b MG Hinchey, CA Rouff, JL Rash y WF Truszkowski (2005) 'Requisitos de un método formal integrado para enjambres inteligentes', en Proceedings of FMICS'05, 5-6 de septiembre de 2005, Lisboa, Portugal . Association for Computing Machinery, págs. 125-133.
- ^ A. Kornai (2009) El álgebra de la semántica léxica . Trabajo presentado en el Encuentro de la Asignación de Matemáticas del Lenguaje de 2009. En In C. Ebert, G. Jäger, J. Michaelis (eds) Proc. XI Taller de Matemáticas del Lenguaje (MOL11) Springer LNCS 6149174-199 [1]
- ^ G. Huet y B. Razet (2008) Tutorial de "Computación con máquinas relacionales" presentado en ICON, diciembre de 2008, Poona "Copia archivada" (PDF) . Archivado desde el original (PDF) el 19 de febrero de 2015 . Consultado el 7 de agosto de 2013 .CS1 maint: copia archivada como título ( enlace )
- ^ P. Goyal, G. Huet, A. Kulkarni, P. Scharf, R. Bunker (2012) "Una plataforma distribuida para el procesamiento de sánscrito" en proc. COLING 2012, págs. 1011–1028 [2]
- ^ M. Stannett (1990) 'Máquinas X y el problema de la detención: construcción de una máquina súper Turing'. Aspectos formales de la informática 2 , págs. 331-41.
- ^ BJ Copeland (2002) 'Hipercomputación'. Mentes y máquinas 12 , págs. 461-502.
- ^ F. Ipate y M. Holcombe (1998) "Un método para refinar y probar especificaciones de máquinas generalizadas". En t. J. Comp. Matemáticas. 68 , págs. 197-219.
- ^ F. Ipate y M. Holcombe (1997) "Un método de prueba de integración que ha demostrado encontrar todas las fallas", International Journal of Computer Mathematics 63 , pp. 159-178.
- ^ J. Barnard, C. Theaker, J. Whitworth y M. Woodward (1995) 'Máquinas X de comunicación en tiempo real para el diseño formal de sistemas en tiempo real', en Proceedings of DARTS '95, Universite Libre, Bruselas, Bélgica, 9 a 11 de noviembre de 2005
- ^ J. Barnard (1996) COMX: Metodología para el diseño formal de sistemas informáticos utilizando máquinas X comunicantes . Tesis doctoral, Universidad de Staffordshire.
- ^ A. Alderson y J. Barnard (1997) 'Sobre cómo hacer un cruce seguro', Informe técnico SOCTR / 97/01 , Escuela de Computación, Universidad de Staffordshire. (Citeseer)
- ^ E. Kehris, G. Eleftherakis y P. Kefalas (2000) 'Uso de máquinas X para modelar y probar programas de simulación de eventos discretos', Proc. Cuarta Conferencia Mundial sobre Circuitos, Sistemas, Comunicaciones y Computadoras , Atenas.
- ^ P. Kefalas, G. Eleftherakis y E. Kehris (2000) 'Comunicación de máquinas X: un enfoque práctico para la especificación modular de sistemas grandes', Informe técnico CS-09/00, Departamento de Ciencias de la Computación , City College, Thessaloniki.
- ^ H. Georgescu y C. Vertan (2000) 'Un nuevo enfoque para comunicar máquinas X de flujo', Journal of Universal Computer Science 6 (5) , págs. 490-502.
- ^ PR Bird y AJ Cowling (1994) 'Modelado de programación lógica utilizando una red de máquinas comunicantes', en Proc. 2º Taller Euromicro sobre Procesamiento En Paralelo y Distribuido, Málaga, 26-28 de enero de 1994 , págs. 156-161. Resumen
- ^ T.Balanescu, AJ Cowling, H. Georgescu, M. Gheorghe, M. Holcombe y C. Vertan (1999) 'Los sistemas de máquinas X comunicantes no son más que máquinas X', Journal of Universal Computer Science , 5 (9 ) , págs. 494-507.
- ^ AJH Simons, KE Bogdanov y WML Holcombe (2001) 'Pruebas funcionales completas usando máquinas de objetos', Informe técnico CS-01-18, Departamento de Ciencias de la Computación , Universidad de Sheffield
- ^ AJH Simons (2006) 'Una teoría de las pruebas de regresión para tipos de objetos compatibles con el comportamiento', Pruebas de software, verificación y confiabilidad , 16 (3) , John Wiley, págs. 133-156.
- ^ M. Stannett y AJH Simons (2002) 'CCS-Augmented X-Machines', Informe técnico CS-2002-04, Departamento de Ciencias de la Computación , Universidad de Sheffield, Reino Unido.