Máquina de estados abstracta

En informática , una máquina de estados abstractos ( ASM ) es una máquina de estados que opera sobre estados que son estructuras de datos arbitrarias ( estructura en el sentido de la lógica matemática , es decir, un conjunto no vacío junto con una serie de funciones ( operaciones ) y relaciones sobre el conjunto).

El método ASM es un método de ingeniería de sistemas práctico y científicamente bien fundamentado que cierra la brecha entre los dos extremos del desarrollo de sistemas:

• la comprensión y formulación humana de problemas del mundo real ( captura de requisitos mediante modelado preciso de alto nivel en el nivel de abstracción determinado por el dominio de aplicación dado).
• el despliegue de sus soluciones algorítmicas mediante máquinas de ejecución de código en plataformas cambiantes (definición de decisiones de diseño, detalles del sistema y de la implementación).

El método se basa en tres conceptos básicos:

• ASM : una forma precisa de pseudocódigo que generaliza las máquinas de estados finitos para operar sobre estructuras de datos arbitrarias.
• modelo de suelo : una forma rigurosa de planos, que sirve como modelo de referencia autorizado para el diseño.
• Refinamiento : un esquema muy general para la instanciación gradual de abstracciones de modelos a elementos concretos del sistema, que proporciona vínculos controlables entre las descripciones cada vez más detalladas en las sucesivas etapas del desarrollo del sistema.

En la concepción original de los ASM, un único agente ejecuta un programa en una secuencia de pasos, posiblemente interactuando con su entorno. Esta noción se extendió para abarcar los cálculos distribuidos , en los que múltiples agentes ejecutan sus programas simultáneamente.

Dado que los modelos ASM modelan algoritmos en niveles de abstracción arbitrarios, pueden proporcionar vistas de alto, bajo e intermedio nivel del diseño de un hardware o software. Las especificaciones de los modelos ASM suelen consistir en una serie de modelos ASM, que comienzan con un modelo base abstracto y avanzan hacia niveles de detalle mayores mediante refinamientos o simplificaciones sucesivas.

Debido a la naturaleza algorítmica y matemática de estos tres conceptos, los modelos ASM y sus propiedades de interés pueden analizarse utilizando cualquier forma rigurosa de verificación (mediante razonamiento) o validación (mediante experimentación, probando la ejecución del modelo).

El concepto de máquinas de Turing asistidas por algoritmos (ASM, por sus siglas en inglés) se debe a Yuri Gurevich , quien lo propuso por primera vez a mediados de la década de 1980 como una forma de mejorar la tesis de Turing de que todo algoritmo es simulado por una máquina de Turing apropiada . Formuló la tesis de las ASM : todo algoritmo, por abstracto que sea, es emulado paso a paso por una ASM apropiada. En el año 2000, Gurevich axiomatizó la noción de algoritmos secuenciales y demostró la tesis de las ASM para ellos. En resumen, los axiomas son los siguientes:

• Los estados son estructuras,
• La transición de estado involucra solo una parte delimitada del estado, y
• Todo es invariante bajo isomorfismos de estructuras. (Las estructuras pueden considerarse álgebras , lo que explica el nombre original de álgebras evolutivas para los ASM).

La axiomatización y caracterización de algoritmos secuenciales se ha extendido a algoritmos paralelos e interactivos.

En la década de 1990, a través de un esfuerzo comunitario, ^{[ 1 ]} se desarrolló el método ASM, que utiliza ASM para la especificación y el análisis formales ( verificación y validación ) de hardware y software informático . Se han desarrollado especificaciones ASM completas de lenguajes de programación (incluidos Prolog , C y Java ) y lenguajes de diseño ( UML y SDL ).

Un relato histórico detallado se puede encontrar en otro lugar. ^{[ 2 ] [ 3 ]}

Existen diversas herramientas de software para la ejecución y el análisis de ASM.

(en orden cronológico desde el año 2000)

• El banco de trabajo ASM
• ASMETA, el metamodelo de máquina de estados abstractos y su conjunto de herramientas.
• AsmL
• CoreASM , disponible en CoreASM, un motor de ejecución ASM extensible
• AsmGofer en Archive.org
• El proyecto de código abierto XASM en SourceForge

• Y. Gurevich, Evolving Algebras 1993: Lipari Guide , E. Börger (ed.), Specification and Validation Methods , Oxford University Press , 1995, 9-36. ( ISBN) 0-19-853854-5)
• Y. Gurevich, Las máquinas de estados abstractos secuenciales capturan algoritmos secuenciales , ACM Transactions on Computational Logic 1(1) (julio de 2000), 77–111.
• R. Stärk, J. Schmid y E. Börger, Java y la máquina virtual Java: definición, verificación, validación , Springer-Verlag , 2001. ( ISBN 3-540-42088-6)
• E. Börger y R. Stärk, Máquinas de estados abstractos: un método para el diseño y análisis de sistemas de alto nivel , Springer-Verlag , 2003. ( ISBN 3-540-00702-4)
• E. Börger y A. Raschke, Compañero de modelado para profesionales de software , Springer-Verlag , 2018. ^{[ 4 ]} ( ISBN 978-3-662-56639-8, doi : 10.1007/978-3-662-56641-1 )

• Máquinas de estados abstractas
• AsmCenter archivado el 13 de septiembre de 2019 en Wayback Machine .
• El conjunto de herramientas TASM: especificación, simulación y verificación formal de sistemas en tiempo real.