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

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.$M_I$$M_\alpha$$M_\beta$

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

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

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.