Máquina de estado abstrato - Abstract state machine

Na ciência da computação , uma máquina de estado abstrato ( ASM ) é uma máquina de estado operando em estados que são estruturas de dados arbitrárias ( estrutura no sentido da lógica matemática , ou seja, um conjunto não vazio junto com uma série de funções ( operações ) e relações sobre o definir).

Visão geral

O Método ASM é um método de engenharia de sistemas prático e cientificamente bem fundamentado que preenche a lacuna entre as duas extremidades do desenvolvimento do sistema:

  • a compreensão humana e a formulação de problemas do mundo real ( captura de requisitos por modelagem precisa de alto nível no nível de abstração determinado pelo domínio de aplicativo dado)
  • a implantação de suas soluções algorítmicas por máquinas de execução de código em plataformas variáveis ​​(definição de decisões de design, sistema e detalhes de implementação).

O método baseia-se em três conceitos básicos:

  • ASM : uma forma precisa de pseudo-código, generalizando máquinas de estado finito para operar sobre estruturas de dados arbitrárias
  • modelo básico : uma forma rigorosa de projetos, servindo como um modelo de referência oficial para o design
  • refinamento : um esquema mais geral para instanciações passo a passo de abstrações de modelo para elementos concretos do sistema, fornecendo links controláveis ​​entre as descrições cada vez mais detalhadas nos estágios sucessivos de desenvolvimento do sistema.

Na concepção original dos ASMs, um único agente executa um programa em uma sequência de etapas, possivelmente interagindo com seu ambiente. Essa noção foi estendida para capturar computações distribuídas , nas quais vários agentes executam seus programas simultaneamente.

Como os ASMs modelam algoritmos em níveis arbitrários de abstração, eles podem fornecer visualizações de alto, baixo e médio nível de um design de hardware ou software. As especificações ASM geralmente consistem em uma série de modelos ASM, começando com um modelo de solo abstrato e prosseguindo para níveis maiores de detalhes em refinamentos ou engrossamentos sucessivos .

Devido à natureza algorítmica e matemática desses três conceitos, os modelos ASM e suas propriedades de interesse podem ser analisados ​​usando qualquer forma rigorosa de verificação (por raciocínio) ou validação (por experimentação, execução de modelos de teste).

História

O conceito de ASMs deve-se a Yuri Gurevich , que o propôs pela primeira vez em meados da década de 1980 como uma forma de aprimorar a tese de Turing de que todo algoritmo é simulado por uma máquina de Turing apropriada . Ele formulou a Tese ASM : cada algoritmo, não importa quão abstrato , é emulado passo a passo por um ASM apropriado. Em 2000, Gurevich axiomatizou a noção de algoritmos sequenciais e provou a tese ASM para eles. Resumindo, os axiomas são os seguintes: estados são estruturas, a transição de estados envolve apenas uma parte limitada do estado e tudo é invariante sob isomorfismos de estruturas. (As estruturas podem ser vistas como álgebras , o que explica o nome original de álgebras em evolução para ASMs.) A axiomatização e a caracterização de algoritmos sequenciais foram estendidas para algoritmos paralelos e interativos.

Na década de 1990, por meio de um esforço comunitário, o método ASM foi desenvolvido, utilizando ASMs para a especificação formal e análise ( verificação e validação ) de hardware e software de computador . Especificações ASM abrangentes de linguagens de programação (incluindo Prolog , C e Java ) e linguagens de design ( UML e SDL ) foram desenvolvidas.

Um relato histórico detalhado pode ser encontrado em outro lugar.

Uma série de ferramentas de software para execução e análise ASM estão disponíveis.

Publicações

Livros

Modelos comportamentais para padrões industriais

Ferramentas

(em ordem histórica desde 2000)

Bibliografia

  • 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, Sequential Abstract State Machines capture Sequential Algorithms , ACM Transactions on Computational Logic 1 (1) (julho de 2000), 77-111.
  • R. Stärk, J. Schmid e E. Börger, Java and the Java Virtual Machine: Definition, Verification, Validation , Springer-Verlag , 2001. ( ISBN  3-540-42088-6 )
  • E. Börger e R. Stärk, Abstract State Machines: A Method for High-Level System Design and Analysis , Springer-Verlag , 2003. ( ISBN  3-540-00702-4 )
  • E. Börger e A. Raschke, Modeling Companion for Software Practitioners , Springer-Verlag , 2018. ( ISBN  978-3-662-56639-8 , doi : 10.1007 / 978-3-662-56641-1 )

Referências

links externos