Is there any work done on developing difference-calculus of Turing Machines (or simpler Formal Languages) I am attempting to develop some notions of a difference-calculus between a notional Ideal Turing Machine conceived by a developer (e.g. whatever is intended by a software developer), call it $M_I$, and the Machines that represent the software which actually gets designed and implemented, say $M_\alpha$ and $M_\beta$, respectively. 

Specifically, my interest is in examining limitations (due to Rice's Theorem for instance) in automated detection of errors in software programs between the Language processed by the ideal machine, and the language processed by the developed/implemented Machines.

Any reference to prior work that works with some notions of exploring differences between two specified Turing Machines, or barring that a lower level Formal Language would be extremely helpful and appreciated; because i'd rather cite than write :-).
As it turns out, there is some fascinating work done in this direction. 

In particular, in 2003, Michael Howard, Jon Pincus, and Jeannette M. Wing's Measuring Relative Attack Surfaces in proceedings of Workshop on Advanced Developments in Software and Systems Security, Taipei, December 2003.  

Further work by the same authors over the years is quite interesting ... For anyone who found my question of interest you can check their work out at http://www.cs.cmu.edu/~pratyus/as.html ... And if you find them interesting, i hope that you will find my work interesting too :)