Wikipédia

Máquina X

modelo de computação teórico

A Máquina-X (XM) é um modelo de computação teórico introduzido por Samuel Eilenberg em 1974.[1] O X em Máquina-X representa o tipo de dados fundamental sobre o qual a máquina opera; por exemplo, a máquina que opera em databases (objetos do tipo database) seria chamada de database-machine. O modelo da Máquina-X é estruturalmente idêntico à máquina de estados finitos, exceto que os símbolos usados para marcar as transições da máquina denotam uma relação do tipo X->X. Realizar uma transição é equivalente a aplicar a relação que a rotulaa (computar um conjunto de mudanças ao tipo de dados X), e percorrer um caminho na máquina corresponde a aplicar todas as relações associadas, uma após a outra.

Teoria Original editar

A teoria original da Máquina-X proposta por Eilenberg era um modelo geral de computação completamente teórico (subsumindo a Máquina de Turing, por exemplo), o qual admitia computações determinísticas, não-determinísticas e não-terminantes. Sua obra seminal [1] inclui muitas variantes do modelo básico da Máquina-X, cada um dos quais generalizava uma máquina de estados finitos de uma maneira ligeiramente diferente.

No modelo mais geral, uma Máquina-X é essencialmente uma "máquina para manipular objetos do tipo X". Suponha que X é algum tipo de dados, chamado tipo de dado fundamental, e que Φ é um conjunto de relações parciais φ: X → X. Uma Máquina-X é uma máquina de estados finitos com suas transições marcadas pelas relações em Φ. Em qualquer dado estado, uma ou mais transições podem ser liberadas se algum domínio da relação associada φi aceita (um sobconjunto dos) os valores atuais de X. Em cada ciclo, todas as transições ativadas são assumidas como utilizadas. Cada caminho reconhecido pela máquina gera uma lista φ1 ... φn de relações. Chamamos a composição φ1 o ... o φn dessas relações de caminho de relações correspondente ao caminho. O comportamento da Máquina-X é definido como a união de todos os comportamentos computados por seus caminhos de relações. De modo geral, isso é não-deterministico, uma vez que aplicar qualquer relação computa um conjunto de saídas em X. No modelo formal, todas as saídas possíveis são consideradas juntas, em paralelo.

Para fins práticos, uma Máquina-X deve descrever alguma computação finita. Uma função de codificação α: Y → X converte de alguma entrada do tipo Y para o estado inicial do tipo X, e uma função de decodificação β: X → Z converte de volta do estado final X para algum tipo de saída Z. Uma vez que o estado inicial de X é populado, a Máquina-X é executada até parar, e as saídas podem então ser observadas. De modo geral, a máquina pode entrar em deadlock (travar), livelock (nunca parar), ou executar uma ou mais computações completas. Por este motivo, pesquisas mais recentes focam em Máquinas-X determinísticas, as quais possuem um comportamento que pode ser controlado e observado mais precisamente.

Exemplo editar

Um compilador com um "olho-mágico" otimizador pode ser considerado como uma máquina para otimizar a estrutura de programas. Nesse Otimizador, a função de codificação α toma o código-fonte da entrada do tipo Y (a fonte do programa) e a carrega na memória de tipo X (árvore de análise sintática). Suponha que a máquina tenha diversos estados, chamados FindIncrements, FindSubExprs e Completed. A máquina começa no estado inicial FindIncrements, o qual é conectado aos outros estados pelas transições: 

 FindIncrements →DoIncrement FindIncrements
 FindIncrements →SkipIncrement FindSubExprs
 FindSubExprs →DoSubExpr FindSubExprs
 FindSubExprs →SkipSubExpr Completed

A relação DoIncrement mapeia a subárvore sintática correspondendo a "x := x + 1" na subárvore otimizada "++x". A relação DoSubExpr mapeia a árvore sintática contendo múltiplas ocorrencias da mesma expressão "x + y ... x + y" em uma versão otimizada com uma variável local para armazenar as repetidas computações "z := x + y; ... z ... z". Estas relações são ativadas somente se X contiver os valores de domínio (subárvores) nas quais elas operam. As relações remanescentes SkipIncrement e SkipSubExpr são nullops (relações identidade) ativadas em casos complementares.

Assim, a máquina Otimizadora vai rodar até completar, primeiro convertendo adições triviais em incrementos (durante o estado FindIncrements), a máquina vai então mover para o estado FindSubExpres e realizar uma séria de remoções de sub-expressões comuns, seguindo depois para o estado final Completed. A função de decodificação β vai então mapear do tipo de memória X (a árvore sintática otimizada) para o tipo de saída Z (código de máquina otimizado).

Convenção editar

Referindo-se ao modelo original de Eilenberg, "Máquina-X" é tipicamente escrita com um "m" minúsculo, pelo sentido de "qualquer máquina para processar X". Quando referindo-se a modelos específicos mais recentes, a convenção é de se usar o "M" maiúsculo como parte do nome próprio da variante.

Década de 1980 editar

O interesse nas Máquinas-X foi revivido no fim dos anos 1980 por Mike Holcombe, [2] quando este percebeu que o modelo era ideal para especificação formal de software, pois ele claramente separa fluxo de controle de processamento. Em um nível de abstração suficientemente alto, o fluxo de controle de uma computação pode ser representado como uma máquina de estados finita, então, para completar a especificação da máquina-X, basta especificar o processamento associado com cada uma das transições da máquina. A simplicidade estrutural do modelo o faz extremamente flexível; outras ilustrações iniciais da ideia incluiam as especificações de interfaces homem-computador de Holcombe,[3] seu modelamento de processos em bioquímica celular, [4] e o modelamento para tomadas de decisão em sistemas de comando militar de Stannett.[5]

Década de 1990 editar

Máquinas-X passaram a receber atenção renovada desde meados da década de 1990, quando a "Stream X-Machine" determinística de Gilbert Laycock[6] serviu como base para especificação de grandes sistemas de software que são completamente testáveis.[7] Outra variante, a "Communicating Stream X-Machine" oferece um modelo útil para testes de processos biológicos[8] e futuros sistemas de satélites swarm. [9]

Década de 2000 editar

Máquinas-X foram aplicadas a analisadores semânticos por Andras Kornai, que modelam o significado de palavras por máquinas "apontadoras", que possuem um membro do conjunto base X distinto.[10] Aplicações para outros ramos da linguística, em particular a reformulação contemporânea de Panini foram liderados por Gerar Huet e seus colegas de trabalho.[11] [12]

Principais variantes editar

A Máquina-X raramente é encontrada em sua forma original, mas sustenta vários modelos subsequentes de computação. O mais influente modelo em teste de software foi a "Stream X-Machine". A NASA discutiu recentemente o uso de uma combinação de "Communicating Stream X-Machines" e o processo de cálculo WSCSS no design e teste de sistemas de de satélite swarm.

Analog X Machine (AXM) editar

A mais antiga variante, a máquina de tempo contínuo Analog X-Machine (AXM) foi introduzida por Mike Stannet em 1990 como um potencial modelo de computação "super-Turing"; [13] ela é consequentemente relacionada a teoria da hipercomputação.[14]

Stream X-Machine (SXM) editar

O modelo mais comumente encontrado de variante da Máquina-X é a "Stream X-Machine" feita por Gilbert Laycock em 1993,[6] que forma a base da teoria do teste completo de software de Mike Holcombe e Florentin Ipate, que garante propriedades de correção conhecidas, uma vez que os testes tenham acabado.[7][15] A "Stream X-Machine" difere do modelo original de Eilenberg no que o tipo de dado fundamental X é da forma Out* x Mem x In*, onde In* é uma sequencia de entrada, Out* é uma sequência de saída, e Mem é a memória.

A vantagem deste modelo é que ele permite que o sistema seja dirigido, um passo por vez, através de seus estados e transições, enquanto observam-se as saídas de cada passo. Estes valores são testemunhas, que garantem que funções em particular tenham sido executadas em cada passo. Como resuldado, sistemas de software complexos podem ser decompostos em uma hierarquia de Stream-X Machines, projetadas de maneira "top-down" e testadas de maneira "bottom-up". Essa abordagem de dividir-e-conquistar para projetar e testar é apoiada pela prova da integração correta de Florentin Ipate,[16] que prova que testar as máquinas em camada independentemente é equivalente a testar o sistema composto.

Communicating X-Machine (CXM) editar

A mais antiga proposta para conectar diversas Máquinas-X em paralelo é o modelo da "Communicating X-Machine" de Judith Barnard, 1995.[17][18] no qual máquinas são conectadas por canais de comunicação nomeados (conhecidos como portas); este modelo existe em ambas as variantes de tempo real e discretas.[19] Versões mais antigas deste trabalho não são completamente formais nem mostram todas as relações de entrada/saída.

Uma "Communicating X-Machine" similar utilizando canais bufferizados foi desenvolvida por Petros Kefalas.[20][21] O foco deste trabalho estava na expressividade da composição dos componentes. A abilidade de redesignar canais significava que alguns dos teoremas de teste das "Stream X-Machines" não eram transferidos.

Communicating Stream X-Machine (CSXM) editar

O primeiro modelo completamente formal da composição das Máquinas-X concorrentes foi proposto em 1999 por Cristina Vertan e Horia Georgescu,[22] com base em trabalhos anteriores sobre automatos comunicantes de Philip Bird e Anthony Cowling.[23] No modelo de Vertan, as máquinas se comunicam indiretamente, por meio de uma matriz de comunicação compartilhada (essencialmente um array de classificação), ao invés de diretamente por meio de canais compartilhados.

Bălănescu, Cowling, Georgescu, Vertan e outros estudaram as propriedades formais deste modelo CSXM em detalhe. Completas relações de entrada/saída podem ser mostradas. A matriz de comunicação estabelece um protocolo para comunicação síncrona. A vantagem disto é que, assim, o processamente de cada máquina é desacoplado da sua comunicação, permitindo o teste separado de cada comportamento. Este modelo composicional foi provado equivalente ao padrão "Stream X-Machine",[24] alavancando assim a teoria de testes anteriormente desenvolvida por Holcombe e Ipate.

Object X-Machine (OXM) editar

Kirill Bogdanov e Anthony Simons desenvolveram diversas variantes de Máquina-X para modelar o comportamento de objetos em sistemas orientados a objetos.[25] Este modelo difere da abordagem da "Stream X-Machine", no que o tipo de dado monolítico X é distribuído e encapsulado por diversos objetos, os quais são serialmente compostos; e sistemas são acionados por invocações de métodos e returnos, em vez de entradas e saídas. Mais trabalhos nesta área envolvem a adaptação da teoria de testes formal ao contexto de hierarquia, que particiona o estado-espaço da superclasse em objetos subclasse estendidos. [26]

O modelo "CCS-augmented X-machine" (CCSXM) foi posteriormente desenvolvido por Simons e Stannet em 2002 para suportar o completo teste de comportamento de sistemas orientados a objetos, na presença de comunicação assíncrona.[27] É experado que este modelo tenha alguma similaridade com a recente proposta da NASA; mas nenhuma comparação definitiva entre os dois modelos foi feita até hoje.

Ver também editar

Referências

  1. ↑ a b S. Eilenberg (1974) Automata, Languages and Machines, Vol. A. Academic Press, London.
  2. ↑ M. Holcombe (1988) 'X-machines as a basis for dynamic system specification', Software Engineering Journal 3(2), pp. 69-76.
  3. ↑ M. Holcombe (1988) 'Formal methods in the specification of the human-machine interface', International J. Command and Control, Communications and Info. Systems. 2, pp. 24-34.
  4. ↑ M. Holcombe (1986) 'Mathematical models of cell biochemistry'. Technical Report CS-86-4, Dept of Computer Science, Sheffield University.
  5. ↑ M. Stannett (1987) 'An organisational approach to decision-making in command systems.' International J. Command and Control, Communications and Info. Systems. 1, pp. 23-34.
  6. ↑ a b Gilbert Laycock (1993) The Theory and Practice of Specification Based Software Testing. PhD Thesis, University of Sheffield. Abstract Arquivado em 5 de novembro de 2007, no Wayback Machine.
  7. ↑ a b M. Holcombe and F. Ipate (1998) Correct Systems - Building a Business Process Solution. Springer, Applied Computing Series.
  8. ↑ A. Bell and M. Holcombe (1996) 'Computational models of cellular processing', in Computation in Cellular and Molecular Biological Systems, eds. M. Holcombe, R. Paton and R. Cuthbertson, Singapore, World Scientific Press.
  9. ↑ M. G. Hinchey, C. A. Rouff, J. L. Rash and W. F. Truszkowski (2005) 'Requirements of an Integrated Formal Method for Intelligent Swarms', in Proceedings of FMICS'05, September 5–6, 2005, Lisbon, Portugal. Association for Computing Machinery, pp. 125-133.
  10. ↑ A. Kornai (2009) The Algebra of Lexical Semantics. Paper presented at the 2009 Meeting of the Assiciation for Mathematics of Language. In In C. Ebert, G. Jäger, J. Michaelis (eds) Proc. 11th Mathematics of Language workshop (MOL11) Springer LNCS 6149 174-199 [1]
  11. ↑ G. Huet and B. Razet (2008) "Computing with Relational Machines" Tutorial presented at ICON, Dec 2008, Poona [2]
  12. ↑ P. Goyal, G. Huet, A. Kulkarni, P. Scharf, R. Bunker (2012) "A Distributed Platform for Sanskrit Processing" In Proc. COLING 2012, pp 1011–1028 [3]
  13. ↑ M. Stannett (1990) 'X-machines and the Halting Problem: Building a super-Turing machine'. Formal Aspects of Computing 2, pp. 331-41.
  14. ↑ B. J. Copeland (2002) 'Hypercomputation'. Minds and Machines 12, pp. 461-502.
  15. ↑ F. Ipate and M. Holcombe (1998) 'A method for refining and testing generalised machine specifications'. Int. J. Comp. Math. 68, pp. 197-219.
  16. ↑ F. Ipate and M. Holcombe (1997) 'An integration testing method that is proved to find all faults', International Journal of Computer Mathematics 63, pp. 159-178.
  17. ↑ J. Barnard, C. Theaker, J. Whitworth and M. Woodward (1995) 'Real-time communicating X-machines for the formal design of real-time systems', in Proceedings of DARTS '95, Universite Libre, Brussels, Belgium, 9–11 November 2005
  18. ↑ J. Barnard (1996) COMX: A methodology for the formal design of computer systems using Communicating X-machines. PhD Thesis, Staffordshire University.
  19. ↑ A. Alderson and J. Barnard (1997) 'On Making a Crossing Safe', Technical Report SOCTR/97/01, School of Computing, Staffordshire University. (Citeseer)
  20. ↑ E. Kehris, G. Eleftherakis and P. Kefalas (2000) 'Using X-machines to model and test discrete event simulation programs', Proc. 4th World Multiconference on Circuits, Systems, Communications and Computers, Athens.
  21. ↑ P. Kefalas, G. Eleftherakis and E. Kehris (2000) 'Communicating X-machines: a practical approach for modular specification of large systems', Technical Report CS-09/00, Department of Computer Science, City College, Thessaloniki.
  22. ↑ H. Georgescu and C. Vertan (2000) 'A new approach to communicating stream X-machines', Journal of Universal Computer Science 6 (5), pp. 490-502.
  23. ↑ P. R. Bird and A. J. Cowling (1994) 'Modelling logic programming using a network of communicating machines', in Proc. 2nd Euromicro Workshop on Parallel and Distributed Processing, Malaga, 26–28 January 1994, pp. 156-161. Abstract
  24. ↑ T.Balanescu, A. J. Cowling, H. Georgescu, M. Gheorghe, M. Holcombe and C. Vertan (1999) 'Communicating X-machines systems are no more than X-machines', Journal of Universal Computer Science, 5 (9), pp. 494-507.
  25. ↑ A. J. H. Simons, K. E. Bogdanov and W. M. L. Holcombe (2001) 'Complete functional testing using object machines', Technical Report CS-01-18, Department of Computer Science, University of Sheffield
  26. ↑ A. J. H. Simons (2006) 'A theory of regression testing for behaviourally compatible object types', Software Testing, Verification and Reliability, 16 (3), John Wiley, pp. 133-156.
  27. ↑ M. Stannett and A. J. H. Simons (2002) 'CCS-Augmented X-Machines', Technical Report CS-2002-04, Department of Computer Science, Sheffield University, UK.

Relatórios técnicos   editar

  • M. Stannett and A. J. H. Simons (2002) Complete Behavioural Testing of Object-Oriented Systems using CCS-Augmented X-Machines. Tech Report CS-02-06, Dept of Computer Science, University of Sheffield. Download
  • J. Aguado and A. J. Cowling (2002) Foundations of the X-machine Theory for Testing. Tech Report CS-02-06, Dept of Computer Science, University of Sheffield. Download
  • J. Aguado and A. J. Cowling (2002) Systems of Communicating X-machines for Specifying Distributed Systems. Tech Report CS-02-07, Dept of Computer Science, University of Sheffield. Download
  • M. Stannett (2005) The Theory of X-Machines - Part 1. Tech Report CS-05-09, Dept of Computer Science, University of Sheffield. Download

Ligações externas editar

Obtida de "https://pt.wikipedia.org/w/index.php?title=Máquina_X&oldid=67190680"