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).

O conceito de ASMs é de crédito de Yuri Gurevich, quem primeiro propôs o mesmo em meados de 1980 como uma melhoria à Tese de Church-Turing na qual todo algoritmo é simulado por uma Máquina de Turing apropriada. Ele formulou a Tese ASM: todo algoritmo, não importa o quanto abstrato, é uma emulação passo-a-passo por uma ASM apropriada. Em 2000, Gurevich axiomatizou a noção de algoritmos seqüenciais, e provou a tese ASM para eles. Vulgarmente dito, os axiomas são os seguintes: estados são estruturas, a transição de estados envolve apenas uma parte delimitada do estado, e tudo é invariante sobre isomorfismo de estruturas (estruturas podem ser vistas como álgebras, as quais explicam o nome original evoluindo álgébras para ASMs). A axiomatização e caracterização de algoritmos seqüenciais foram estendidas para computação paralela e algoritmos interativos.

Nos anos 1900, por um esforço comunitário, o método ASM foi desenvolvido, usando ASMs para a especificação formal e análise (verificação e validação) de hardware de computadores e software. Especificações ASM compreensivas de linguagens de programação (incluindo Prolog, C, e Java) e design de linguagens (UML e SDL) foram desenvolvidas. Um relato histórico detalhado pode ser encontrado no capítulo 9 do livro AsmBook ou neste artigo.

Um número de ferramentas de software para execução e análise de ASM estão disponíveis.

• AsmBook: E.Börger, R.Stärk. Abstract State Machines: A Method for High-Level System Design and Analysis

• JBook: R.Stärk, J.Schmid, E.Börger. Java and the Java Virtual Machine: Definition, Verification, Validation

• Procedimentos/Artigos em Periódicos (desde 2000)
  • 2008: Springer LNCS 5238 Abstract State Machines, B and Z
  • 2007: J.UCS Special Issue with and http://osys.grm.hia.no/asm07/proceedings Selected Papers from ASM'07
  • 2006: Springer LNCS 5115 Rigorous Methods for Software Construction and Analysis, ASM and B Dagstuhl Seminar
  • 2005: Fundamenta Informatica Special Issue with Selected Papers from ASM'05 (electronic proceedings)
  • 2004: Springer LNCS 3052 Abstract State Machines 2004
  • 2003: Springer LNCS 2589 Abstract State Machines 2003: Advances in Theory and Practice
  • 2003: TCS special Issue with Selected Papers from ASM'03
  • 2002: Dagstuhl Seminar Report Theory and Applications of Abstract State Machines
  • 2001: J.UCS 7.11 Special Issue with Selected Papers from ASM'01
  • 2000: Springer LNCS 1912 Abstract State Machines: Theory and Applications

• Estudo de casos comparativos com contribuições da ASM
  • Steam-Boiler Control: Specification Case Study, Springer LNCS 1165
  • Production Cell: Software Development Case Study, ASM model
  • Railcrossing: Formal Methods for Real-Time Computing, ASM model
  • Light Control: Requirements Engineering Case Study, Dagstuhl Seminar
  • Invoicing: Requirements Capture Case Study

• OMG for BPMN (version 2006): Springer LNCS 5316
• OASIS for BPEL: IJBPMI 1.4 (2006)
• ECMA for C#: TCS 336 (2006)
• ITU-T for SDL-2000: formal semantics of SDL-2000 and Formal Definition of SDL-2000 - Compiling and Running SDL Specifications as ASM Models
• IEEE for VHDL93: E.Boerger, U.Glaesser, W.Mueller. Formal Definition of an Abstract VHDL'93 Simulator by EA-Machines. In: Carlos Delgado Kloos and Peter T.~Breuer (Eds.), Formal Semantics for VHDL, pp. 107–139, Kluwer Academic Publishers, 1995
• ISO for Prolog: A mathematical definition of full Prolog

(em ordem histórica desde 2000)

• ASMETA, the Abstract State Machine Metamodel and its tool set
• AsmL
• CoreASM, disponível em CoreASM, an extensible ASM execution engine
• AsmGofer
• The XASM open source project

• 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 and 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 and 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) (July 2000), 77-111.

• Abstract State Machines
• AsmCenter
• The TASM toolset: specification, simulation, and formal verification of real-time systems