eighty-twenty

This work explores the middle ground between strict up-front formal methods and just using model checking as a debugging tool. The former doesn’t cope well with real-world projects — changes in the implementation don’t end up getting propagated all the way back to the formal model — and the latter, while enabling round-tripping to some degree, only provides a way of reasoning about fairly weak properties of the program.

L. Lamport’s TLA is used here to analyse actual software program code. It’s really only been used to analyse algorithms (ie. small isolated program fragments) and hardware specifications before.

TLA+ is a framework based on TLA that has been extended to be able to model real programs. The temporal logic in TLA is really not the main thrust — it’s there so that the temporal logic stuff fades into the background, leaving you to get real work done.

So this project attempts to allow pulling back all the way to algorithms from real code — not just having to stop at some limited properties of the program — the idea being to give the power of full up-front formal methods with the flexibility of the “debugging” approach.

The project models the C language. The model is then used as an interpreter for the program we’re ultimately interested in. The model-checker TLC tells you which transformations on your program are meaning preserving; the user then goes through the program transforming it to successively more and more abstract high-level code. Ultimately you end up with a high-level formal model of the low-level program, about which quite interesting questions can be asked and answered within the TLA+ framework.