En informática , una máquina de estados abstractos ( 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, un conjunto no vacío junto con una serie de funciones ( operaciones ) y relaciones sobre el colocar).
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 del sistema:
- la comprensión humana y la formulación de problemas del mundo real ( captura de requisitos mediante modelos precisos 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 estado finito 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 más general para instanciaciones escalonadas de abstracciones del modelo a elementos concretos del sistema, proporcionando 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 solo agente ejecuta un programa en una secuencia de pasos, posiblemente interactuando con su entorno. Esta noción se amplió para capturar cálculos distribuidos , en los que varios agentes ejecutan sus programas al mismo tiempo.
Dado que los ASM modelan algoritmos 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 a menudo consisten en una serie de modelos de ASM, comenzando con un modelo de suelo abstracto y avanzando a mayores niveles de detalle en sucesivos refinamientos o refinamientos .
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 (por razonamiento) o validación (por experimentación, prueba de 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 adecuada . Formuló la Tesis de ASM : cada algoritmo, no importa 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 de ASM para ellos. En términos generales, los axiomas son los siguientes: los estados son estructuras, la transición de estado involucra solo una parte limitada del estado y todo es invariante bajo isomorfismos de estructuras. (Las estructuras pueden verse como álgebras , lo que explica el nombre original de álgebras evolutivas para ASM). La axiomatización y caracterización de algoritmos secuenciales se han extendido a algoritmos paralelos e interactivos.
En la década de 1990, gracias a 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 completas 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 el AsmBook (Capítulo 9) o en este artículo .
Se encuentran disponibles varias herramientas de software para la ejecución y el análisis de la MAPE.
Publicaciones
Libros
- AsmBook: Egon Börger , Robert Stärk . Máquinas de estado abstracto: 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
- Proceedings / Journal Issues (desde 2000)
- 2008: Springer LNCS 5238 Abstract State Machines, B y Z
- 2007: Edición especial de J.UCS con y http://osys.grm.hia.no/asm07/proceedings 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 ( procedimientos electrónicos )
- 2004: Springer LNCS 3052 Abstract State Machines 2004
- 2003: Springer LNCS 2589 Abstract State Machines 2003: Avances en la teoría y la práctica
- 2003: Edición especial de TCS con artículos seleccionados de ASM'03
- 2002: Informe del seminario Dagstuhl Teoría y aplicaciones de las máquinas de estado abstracto
- 2001: Edición especial de J.UCS 7.11 con artículos seleccionados de ASM'01
- 2000: Springer LNCS 1912 Abstract State Machines: teoría y aplicaciones
- Estudios de caso comparativos con contribuciones de MAPE
- Control de calderas de vapor: estudio de caso de especificación , Springer LNCS 1165
- Célula 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 luz: estudio de caso de ingeniería de requisitos , seminario Dagstuhl
- Facturación: caso de estudio de captura de requisitos
Modelos de comportamiento para estándares industriales
- Dios mío 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.), Semántica formal para VHDL , págs. 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)
- ASMETA, el metamodelo Abstract State Machine y su conjunto de herramientas
- AsmL
- CoreASM , disponible en CoreASM, un motor de ejecución ASM extensible
- AsmGofer
- El proyecto de código abierto XASM
Referencias
- 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 )
- E. Börger y R. Stärk, Abstract State Machines: A Method for High-Level System Design and Analysis , Springer-Verlag , 2003. ( ISBN 3-540-00702-4 )
- R. Stärk, J. Schmid y E. Börger, Java and the Java Virtual Machine: Definition, Verification, Validation , Springer-Verlag , 2001. ( ISBN 3-540-42088-6 )
- Y. Gurevich, Sequential Abstract State Machines capture Sequential Algorithms , ACM Transactions on Computational Logic 1 (1) (julio de 2000), 77-111.
enlaces externos
- Máquinas de estado abstracto
- AsmCenter
- El conjunto de herramientas TASM: especificación, simulación y verificación formal de sistemas en tiempo real