Máquina de estado abstracto

En informática , una máquina de estados abstractos (en inglés máquinas de estados abstractos o ASM ) es un autómata finito cuyos estados no solo tienen nombres, sino estructuras en el sentido de la lógica matemática , es decir, conjuntos no vacíos con funciones , operaciones y relaciones . Las estructuras pueden verse como álgebras, lo que explica el nombre de álgebras evolutivas que se le dio inicialmente a los ASM.

Principios

El método ASM es un método práctico de ingeniería de sistemas con base científica que une los dos aspectos del desarrollo del sistema:

El método se basa en tres conceptos:

Inicialmente, las MAPE están diseñadas para un solo agente ; Más tarde, el concepto se extendió a los cálculos distribuidos , donde varios agentes ejecutan sus programas simultáneamente. El ASM modela los algoritmos a niveles arbitrarios de abstracción. Por lo tanto, pueden proporcionar descripciones de nivel alto, medio o bajo. Las especificaciones de ASM a menudo se componen de un conjunto de modelos de ASM , comenzando con un modelo base abstracto y progresando a niveles más detallados mediante refinamientos sucesivos.

Debido a la naturaleza algorítmica y matemática de estos tres conceptos, los modelos ASM y sus propiedades pueden analizarse utilizando cualquier método riguroso de verificación (por razonamiento) o validación (por experimentación y pruebas de ejecución del modelo).

Aplicaciones

En la compilación , el modelo se utiliza para la descripción de la semántica y, por lo tanto, ayuda a garantizar la preservación de esta semántica durante la traducción. De manera más general, el modelo permite, durante la fase de análisis y diseño del desarrollo de software, una descripción formal de los requisitos funcionales. El enfoque matemático mejora la verificación y la reutilización. La formalización de estados abstractos también se utiliza al diseñar circuitos complejos en lógica secuencial .

Evolución del modelo

ASM fue introducido a mediados de la década de 1980 por Yuri Gurevich  (en) de Microsoft, que los ofreció como un medio para lograr la tesis de Church , que cualquier algoritmo puede ser simulado por una máquina de Turing propiamente dicha. Gurevich lo formuló en la forma que se ha convertido en la "tesis ASM"  : cualquier algoritmo, sea cual sea su nivel de abstracción , puede ser objeto de una emulación progresiva por un ASM apropiado. En 2000, Gurevich da una axiomatización de la noción de algoritmo secuencial y demuestra la “tesis de ASM” para esta clase. Los axiomas son, aproximadamente, los siguientes: los estados son estructuras, y una transición de estado solo concierne a una parte limitada del estado, y finalmente todo es invariante por isomorfismo de estructuras. La axiomatización y caracterización de algoritmos secuenciales se extendió luego a algoritmos paralelos e interactivos.

En la década de 1990, el método ASM se utilizó en la especificación formal , verificación y validación de hardware y software . Se desarrollan especificaciones completas de ASM para lenguajes de programación como Prolog , C y Java , y lenguajes de diseño como UML y SDL ) o VHDL . Se puede encontrar una historia detallada en el capítulo 9 del libro Abstract State Machines , 2003 o en el artículo de Egon Börger, "  Los orígenes y el desarrollo del método ASM para alto nivel  ", Journal of Universal Computer Science , vol.  8, n o  1,2002( leer en línea ). Se encuentran disponibles varias herramientas de software para el análisis y la ejecución de MAPE.

Notas y referencias

  1. Yuri Gurevich, "Una nueva tesis", resúmenes, American Mathematical Society Vol. 6, no 4, agosto de 1985), página 317, resumen 85T-68-203.
  2. Yuri Gurevich, "  Las máquinas secuenciales de estado abstracto capturan algoritmos secuenciales  ", Transacciones ACM sobre lógica computacional , Asociación de Maquinaria de Computación (ACM), vol.  1, n o  1,julio 2000, p.  77-111 ( DOI  10.1145 / 343369.343384 , leer en línea ).
  3. Egon Börger y Dean Rosenzweig, “  Una definición matemática de prólogo completo  ”, Science of Computer Programming , vol.  24, n o  3,Junio ​​de 1995, p.  249-286 ( DOI  10.1016 / 0167-6423 (95) 00006-e )
  4. Egon Börger, Nicu G. Fruja, Vincenzo Gervasi y Robert F. Stärk, “  Una definición modular de alto nivel de la semántica de C #  ”, Informática teórica , vol.  336, n hueso  2-3,Mayo de 2005, p.  235-284 ( ISSN  0304-3975 , DOI  10.1016 / j.tcs.2004.11.008 ).
  5. Robert F. Stärk, Joachim Schmid y Egon Börger, Java y la máquina virtual Java: definición, verificación, validación , Springer,2001, 381  p. ( ISBN  978-3-540-42088-0 ).
  6. Uwe Glässer, Reinhard Gotzhein y Andreas Prinz, “  La semántica formal de SDL-2000: estado y perspectivas  ”, Computer Networks , vol.  42, n o  3,Junio ​​de 2003, p.  343-358 ( ISSN  1389-1286 , DOI  10.1016 / s1389-1286 (03) 00247-0 ).
  7. Robert Eschbach, Uwe Glässer, Reinhard Gotzhein, Martin von Löwis y Andreas Prinz, "  Definición formal de SDL-2000: compilación y ejecución de especificaciones SDL como modelos ASM  ", Journal of Universal Computer Science , vol.  7, n o  11, 2001( leer en línea ).
  8. Egon Börger, Uwe Glässer y Wolfgang Muller, “Una definición formal de un simulador abstracto VHDL'93 por EA-Machines” , en Carlos Delagado Kloos y Peter T. Breuer (eds), Semántica formal para VHDL , Springer,1995( DOI  10.1007 / 978-1-4615-2237-9_5 ) , pág.  107-139

Bibliografía

Implementaciones

enlaces externos