[TechTalkFollowup] UML vs. TLA+

I just listened to http://www.se-radio.net/2014/04/episode-203-leslie-lamport-on-distributed-s… and Leslie Lamport 's comparison of UML vs. his TLA+ system reminded me of Michael's talk about PlantUML. I don't think I can do TLA+ justice so it would be best to listen to the podcast above but I'd like to point to a practical use of TLA+ he mentioned at Amazon. According to https://groups.google.com/d/msg/tlaplus/C7Rmka3iSGE/zLQjQh0NeSEJ Chris Newcombe will soon be publishing a paper called "Why Amazon Chose TLA+". He goes on to say: "Part of my evaluation is already available, in a talk that I gave at HPTS (bi-annual workshop on High Performance Transaction Systems) in 2011 Slides including notes : http://hpts.ws/papers/2011/sessions_2011/Debugging.pdf Specifications for 2 'real world' algorithms for transaction isolation, in both Alloy and TLA+ : http://hpts.ws/papers/2011/sessions_2011/amazonbundle.tar.gz " His LinkedIn profile at http://www.linkedin.com/pub/chris-newcombe/1/a08/b33 says "Successfully introduced formal methods to Amazon, using Leslie Lamport's method (TLA+ and PlusCal)" That tarball has some interesting TLA+ examples (textbookSnapshotIsolation.tla and serializableSnapshotIsolation.tla, attached.) They're reminiscent of Michael's PlantUML examples but more rigorous and mathematical, I'd say... For more on TLA+ see http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html Phil On Sun, Jan 12, 2014 at 12:13 PM, Bar-sinai, Michael <mbarsinai(a)iq.harvard.edu> wrote: -- Philip Durbin Software Developer for http://thedata.org http://www.iq.harvard.edu/people/philip-durbin