Máquina de estados abstractos

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

Descripción general

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 humana y la formulación de los problemas del mundo real (requisitos captados por modelos precisos de alto nivel a 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ódigos en plataformas cambiantes (definición de decisiones de diseño, detalles de sistema e implementación).

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

• ASM: una forma precisa de pseudo-código, generalizando máquinas estatales finitas para operar sobre estructuras de datos arbitrarias
• modelo de tierra: una forma rigurosa de planos, sirviendo como modelo de referencia autorizado para el diseño
• refinamiento: un esquema más general para instantáneas graduales de abstracciones modelo a elementos del sistema concreto, proporcionando enlaces controlables entre las descripciones más y más detalladas en las etapas sucesivas 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 amplió para abarcar cálculos distribuidos, en los que varios agentes ejecutan sus programas al mismo tiempo.

Dado que los algoritmos modelo ASMs a niveles arbitrarios de abstracción, pueden proporcionar vistas de alto nivel, de bajo nivel y de nivel medio de un diseño de hardware o software. Las especificaciones ASM con frecuencia consisten en una serie de modelos ASM, comenzando con un resumen modelo de tierra y avanzar a mayores niveles de detalle en refinaciones o en ensuciamientos sucesivos.

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

Historia

El concepto de ASM 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 cada algoritmo es simulado por una máquina de Turing apropiada. Formuló la Tesis ASM: cada algoritmo, sin importar cuán abstracto sea, es emulado paso a paso por un ASM apropiado. En 2000, Gurevich axiomatizó la noción de algoritmos secuenciales y demostró la tesis ASM para ellos. En términos generales, los axiomas son los siguientes:

• estados son estructuras,
• la transición estatal implica sólo una parte limitada del estado, y
• todo es invariable bajo isomorfismos de estructuras. (Las estructuras se pueden ver como álgebras, lo que explica el nombre original álgebras en evolución para ASMs.)

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

En la década de 1990, a través de un esfuerzo comunitario, se desarrolló el método ASM, utilizando ASM para la especificación y análisis formal (verificación y validación) de hardware y software de computadora. Se han desarrollado especificaciones ASM integrales de lenguajes de programación (incluidos Prolog, C y Java) y lenguajes de diseño (UML y SDL).

Se puede encontrar un relato histórico detallado en otro lugar.

Hay disponibles varias herramientas de software para la ejecución y el análisis de ASM.

Publicaciones

Libros

• AsmBook: Egon Börger, Robert Stärk. Abstract State Machines: A Method for High-Level System Design and Analysis
• R.Stärk, J.Schmid, E.Börger. Java y la máquina virtual de Java: Definición, verificación, validación
• Proceedings/Journal Issues (since 2000)
  • 2008: Springer LNCS 5238 Abstract State Machines, B and Z
  • 2007: J.UCS Edición Especial con Documentos seleccionados de ASM'07
  • 2006: Springer LNCS 5115 Métodos rigurosos para la construcción y análisis de software, Seminario ASM y B Dagstuhl
  • 2005: Fundamenta Informatica Special Issue with Selected Papers from ASM'05 (electronic proceedings)
  • 2004: Springer LNCS 3052 Abstract State Machines 2004
  • 2003: Springer LNCS 2589 Abstract State Machines 2003: Advances in Theory and Practice
  • 2003: TCS edición especial con documentos seleccionados de ASM'03
  • 2002: Dagstuhl Seminar Report Theory and Applications of Abstract State Machines
  • 2001: J.UCS 7.11 Edición especial con documentos seleccionados de ASM'01
  • 2000: Springer LNCS 1912 Abstract State Machines: Teoría y Aplicaciones
• Estudios de casos comparativos con contribuciones ASM
  • Control de bobinado de vapor: Estudio de caso de especificación, LNCS Springer 1165
  • Unidad de producción: Estudio de caso de desarrollo de software, modelo ASM
  • Railcrossing: Métodos formales para la computación en tiempo real, modelo ASM
  • Control de la luz: Estudio de caso de ingeniería de requisitos, Seminario Dagstuhl
  • Facturación: Requisitos Capture Case Study

Modelos conductuales para estándares industriales

• OMG for BPMN (version 2006): Springer LNCS 5316
• OEAIS for BPEL: IJBPMI 1.4 (2006)
• ECMA para C#: "Una definición modular de alto nivel de la semántica de C interino" doi:10.1016/j.tcs.2004.11.008
• ITU-T for SDL-2000: formal semantics of SDL-2000 and Formal Definition of SDL-2000 - Compiling and Running SDL Especificaciones como modelos ASM
• IEEE para VHDL93: E.Boerger, U.Glaesser, W.Mueller. Definición formal de un simulador abstracto VHDL'93 por EA-Machines. En: Carlos Delgado Kloos y Peter T.~Breuer (Eds.), Semántica formal para VHDL, pp. 107–139, Kluwer Academic Publishers, 1995
• ISO para Prolog: "Una definición matemática de Prolog completo" doi:10.1016/0167-6423(95)00006-E

Herramientas

(en orden histórico desde 2000)

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