Máquinas de Estado Abstratas (ASM, do inglês Abstract State Machines), introduzidas por Yuri Gurevich, são um conceito poderoso e elegante, baseado em Álgebras Evolutivas, para modelagem matemática e verificação formal de sistemas dinâmicos discretos.
A metodologia apresentada neste tutorial provê recursos expressivos para especificar a semântica operacional de sistemas dinâmicos discretos, em um nível de abstração natural e de uma maneira direta e essencialmente livre de codificação. Com isso, objetiva-se diminuir a distância que há entre modelos formais de computação e métodos práticos de especificação.
Os principais tópicos abordados neste tutorial são: (i) conceituação do modelo ASM; (ii) a metodologia ASM, apresentada de maneira formal e ilustrada com vários exemplos; (iii) a utilização de ASM para definir semântica operacional de linguagens programação, exemplificada com a definição de uma linguagem imperativa de pequeno porte; (iv) ASM Multiagentes, que são uma extensão do modelo para sistemas distribuídos; (v) uma avaliação da metodologia, comparando com outras existentes; (vi) uma amostra do que está sendo pesquisado em ASM no momento. ASM já foram utilizadas na definição formal de várias linguagens de programação importantes, entre elas, Java, C e Prolog.
Como principais vantagens em se utilizar a metodologia encontramos: precisão inerente ao modelo formal; facilidade de demonstração
de propriedades da especificação; generalidade; facilidade de aprendizado; facilidade de leitura e escrita; escalabilidade do modelo;
e capacidade de execução da especificação.