Máquina de estados abstratos

Em ciência da computação, uma máquina de estados abstratos (ASM) é uma máquina de estados finitos operando em estados que são estruturas de dados arbitrárias (estruturas no sentido de lógica matemática, que é um conjunto não-vazio juntamente com um número de funções (operações sobre o conjunto) e relações). O Método ASM é um método de engenharia de sistemas prático e cientificamente bem-embasado que diminui a lacuna entre as duas extremidades do desenvolvimento de sistema: * o entendimento humano e a formulação de problemas do mundo-real (análise de requerimentos por uma modelagem acurada de alto nível com o nível de abstração determinada pelo domínio da aplicação) * a implementação de suas soluções algorítmicas por máquinas de execução de código em plataformas de mudança (definição de decisão de projeto, sistema, e detalhes de implementação). O método é construído em cima de três conceitos básicos: * ASM: uma forma precisa de pseudo-código, generalizando Máquina de Estados Finitos para operar sobre estruturas arbitrárias de dados; * modelo terra: uma forma rigorosa de blueprints, servindo de modelo de referência de autorização para o design; * refinamento: um esquema mais geral para instanciações passo-a-passo de abstrações de modelo para elementos concretos de sistema, provendo ligações controláveis e descrições mais detalhadas nos sucessivos estágios de desenvolvimento de sistema. Na concepção original de ASMs, um único agente executa um programa em uma seqüência de passos, possivelmente interagindo com o seu ambiente. Esta noção foi estendida para capturar processamento distribuído, no qual múltiplos agentes executam seus programas concorrentemente. Já que modelos algorítmicos ASM em níveis arbitrários de abstração, podem prover visões de baixo, alto, e médio níveis do projeto de um hardware e software, especificações ASM freqüentemente consistem em uma série de modelos ASM, começando com um modelo terra abstrato e procedendo para níveis maiores de detalhes em sucessivos refinamentos ou detalhamentos. Devido à natureza algorítmica e matemática destes três conceitos, modelos ASM e suas propriedades de interesse podem ser analisadas usando quaisquer forma rigorosa de verificação (pelo raciocínio) ou validação (por experimentação, testando modelos de execução).