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

  • 4
    $\begingroup$ Sounds like model-based testing. One develops a model of the desired system and then uses this to generate tests for the actual system. $\endgroup$ Commented Dec 14, 2011 at 7:24
  • $\begingroup$ @DaveClarke thank you for the cross-reference to model-based testing, it should've occurred to me there are definite benefits to looking at model-based testing ... i wonder if i start with just FSA and build up i may be able to utilize a lot of the existing theory on fault modelling. (just thinking out loud) $\endgroup$ Commented Dec 14, 2011 at 9:35
  • 1
    $\begingroup$ I'd also look at the theories of program refinement and the refinement calculus. R.-J. Back and J. von Wright have developed this theory. In the world of concurrent programming, there is the related concept of action refinement. $\endgroup$ Commented Dec 14, 2011 at 14:57
  • $\begingroup$ @MartinBerger thank you for the suggestion of looking into action refinement. Specifically Action Refinement in Process Algebra and Security Issues dsi.unive.it/~srossi/Papers/lopstr07.pdf was an interesting find for sure! $\endgroup$ Commented Dec 16, 2011 at 15:16
  • $\begingroup$ General update: The technical report "Attack Modeling for Information Security and Survivability" by Moore, A.P. and Ellison, R.J. and Linger, R.C.; provides a good starting basis. P.S. I may end up posting an answer to my own question as derived by all the wonderful suggestions by everyone.. Is that usual? $\endgroup$ Commented Dec 16, 2011 at 15:21

2 Answers 2


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


I think that software model checking, in the vein of Alloy, is probably related to what you're looking for. You write a model, and also a specification that the model should satisfy, and check if they're related appropriately.

  • $\begingroup$ Alloy is a very interesting suggestion :) $\endgroup$ Commented Dec 15, 2011 at 1:33

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.