En informática , una máquina de estados abstracta ( 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).
Descripción general
El método ASM es un método de ingeniería de sistemas práctico y científicamente bien fundamentado que une los dos extremos del desarrollo de sistemas:
- La comprensión y formulación humana de problemas del mundo real ( captura de requisitos mediante un 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 ejecutoras de código en plataformas cambiantes (definición de decisiones de diseño, detalles del sistema y de 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 tierra : una forma rigurosa de planos, que sirve como modelo de referencia autorizado para el diseño
- refinamiento : un esquema más general para instanciaciones paso a paso de abstracciones de modelos a elementos concretos del sistema, proporcionando vínculos controlables entre las descripciones cada vez 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 los cálculos distribuidos , en los que varios agentes ejecutan sus programas simultáneamente.
Dado que los algoritmos de modelado de ASM se basan en niveles arbitrarios de abstracción, pueden proporcionar vistas de alto, bajo y medio nivel de un diseño de hardware o software. Las especificaciones de ASM suelen constar de una serie de modelos de ASM, comenzando con un modelo básico abstracto y avanzando hacia niveles mayores de detalle en sucesivos refinamientos o ajustes.
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, pruebas de ejecuciones del modelo).
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 lo abstracto que sea, es emulado paso a paso por una ASM apropiada. 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:
- Los estados son estructuras,
- La transición de estado involucra sólo una parte limitada del estado, y
- Todo es invariante bajo isomorfismos de estructuras. (Las estructuras pueden considerarse como álgebras , lo que explica el nombre original de álgebras evolutivas para los ASM).
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, [1] se desarrolló el método ASM, que utiliza ASM para la especificación formal y el análisis ( verificación y validación ) de hardware y software de computadoras. 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. [2] [3]
Hay varias herramientas de software disponibles para la ejecución y análisis de ASM.
Publicaciones
Libros
- AsmBook: Egon Börger , Robert Stärk. Máquinas de estados abstractos: un método para el diseño y análisis de sistemas de alto nivel
- JBook: R.Stärk, J.Schmid, E.Börger. Java y la máquina virtual Java: definición, verificación, validación
- Actas/Números de revistas (desde 2000)
- 2008: Springer LNCS 5238 Máquinas de estados abstractos, B y Z
- 2007: Número especial de la J.UCS con artículos 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: Número especial de Fundamenta Informatica con artículos seleccionados de ASM'05 (actas electrónicas)
- 2004: Springer LNCS 3052 Máquinas de estados abstractos 2004
- 2003: Springer LNCS 2589 Máquinas de estados abstractos 2003: avances en teoría y práctica
- 2003: Número especial de TCS con artículos seleccionados de ASM'03
- 2002: Informe del seminario Dagstuhl sobre teoría y aplicaciones de las máquinas de estados abstractos
- 2001: Número especial de la J.UCS 7.11 con artículos seleccionados de ASM'01
- 2000: Springer LNCS 1912 Máquinas de estados abstractos: teoría y aplicaciones
- Estudios de casos comparativos con contribuciones de ASM
- Control de calderas de vapor: estudio de caso de especificación, Springer LNCS 1165
- Célula de producción: caso de estudio de desarrollo de software, modelo ASM
- Railcrossing: métodos formales para computación en tiempo real, modelo ASM
- Control de iluminación: estudio de caso de ingeniería de requisitos, seminario de Dagstuhl
- Facturación: estudio de caso de captura de requisitos
Modelos de comportamiento para estándares industriales
- OMG para BPMN (versión 2006): Springer LNCS 5316
- OASIS para BPEL: IJBPMI 1.4 (2006)
- ECMA para C#: "Una definición modular de alto nivel de la semántica de C♯" doi :10.1016/j.tcs.2004.11.008
- ITU-T para SDL-2000: semántica formal de SDL-2000 y definición formal de SDL-2000: compilación y ejecución de especificaciones SDL 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.), Formal Semantics for 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 de ASM
- ASMETA, el metamodelo de máquina de estados abstractos y su conjunto de herramientas
- AML (lenguaje de señas americano)
- CoreASM , disponible en CoreASM, un motor de ejecución ASM extensible
- AsmGofer en Archive.org
- El proyecto de código abierto XASM en SourceForge
Bibliografía
- Y. Gurevich, Evolving Algebras 1993: Guía de Lipari , E. Börger (ed.), Métodos de especificación y validación , 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)
Referencias
Enlaces externos
- Máquinas de estados abstractos
- 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
