Existe algum trabalho realizado no desenvolvimento de cálculo de diferença de máquinas de Turing (ou linguagens formais mais simples)

8

Estou tentando desenvolver algumas noções de cálculo de diferença entre uma Máquina Ideal de Turing ideal concebida por um desenvolvedor (por exemplo, o que se pretende que um desenvolvedor de software), chame de , e as Máquinas que representam o software que realmente é projetado e implementado, digamos M α e M β , respectivamente.MIMαMβ

Especificamente, meu interesse é examinar limitações (devido ao Teorema de Rice, por exemplo) na detecção automatizada de erros em programas de software entre o Idioma processado pela máquina ideal e o idioma processado pelas Máquinas desenvolvidas / implementadas.

Qualquer referência a trabalhos anteriores que funcionem com algumas noções de exploração de diferenças entre duas Máquinas de Turing especificadas ou barrando que uma Linguagem Formal de nível inferior seria extremamente útil e apreciada; porque eu prefiro citar a escrever :-).

Ahmed Masud
fonte
4
Parece teste baseado em modelo . Um deles desenvolve um modelo do sistema desejado e depois o usa para gerar testes para o sistema real.
perfil completo de Dave Clarke
@DaveClarke obrigado pela referência cruzada ao teste baseado em modelo, deveria ter me ocorrido que há benefícios definitivos em olhar para o teste baseado em modelo ... Será que eu começo com apenas FSA e desenvolvo capaz de utilizar grande parte da teoria existente sobre modelagem de falhas. (só de pensar em voz alta)
Ahmed Masud
1
Eu também examinaria as teorias do refinamento de programas e o cálculo de refinamento. R.-J. Back e J. von Wright desenvolveram essa teoria. No mundo da programação simultânea, existe o conceito relacionado de refinamento de ação.
Martin Berger
@MartinBerger, obrigado pela sugestão de analisar o refinamento da ação. Refinamento de ação especificamente em álgebra de processos e questões de segurança dsi.unive.it/~srossi/Papers/lopstr07.pdf foi uma descoberta interessante, com certeza!
Ahmed Masud
Atualização geral: O relatório técnico "Modelagem de Ataques para Segurança e Sobrevivência da Informação", de Moore, AP e Ellison, RJ e Linger, RC; fornece uma boa base inicial. PS: Eu posso acabar postando uma resposta para minha própria pergunta, derivada de todas as sugestões maravilhosas de todos. Isso é normal?
Ahmed Masud

Respostas:

3

Como se vê, há algum trabalho fascinante feito nessa direção.

Em particular, em 2003, Michael Howard, Jon Pincus e Jeannette M. Wing, que medem as superfícies de ataque relativo nos procedimentos do Workshop sobre desenvolvimentos avançados em segurança de software e sistemas, Taipei, dezembro de 2003.

Trabalhos futuros dos mesmos autores ao longo dos anos são bastante interessantes ... Para quem encontrou minha pergunta de interesse, confira o trabalho deles em http://www.cs.cmu.edu/~pratyus/as.html . E se você os achar interessantes, espero que você ache meu trabalho interessante também :)

Ahmed Masud
fonte
2

Eu acho que a verificação do modelo de software, na veia do Alloy , provavelmente está relacionada ao que você está procurando. Você escreve um modelo e também uma especificação que o modelo deve atender e verifica se eles estão relacionados adequadamente.

Sam Tobin-Hochstadt
fonte
Alloy é uma sugestão muito interessante :)
Ahmed Masud 15/12