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:
Hello everyone,
The slides and code for Thursday talk (diagrams etc.), with some internal projects
mentions removed, are available here:
http://www.mbarsinai.com/blog/2014/01/12/draw-more-work-less/
-- Michael
(Thanks @philip_durbin for suggesting to post it)
_______________________________________________
TechTalkFollowup mailing list
TechTalkFollowup(a)lists.iq.harvard.edu
This list is shared with the public. Please do not discuss Harvard Confidential business
on this list.
To unsubscribe from this list or get other information:
https://lists.iq.harvard.edu/mailman/listinfo/techtalkfollowup
--
Philip Durbin
Software Developer for
http://thedata.org
http://www.iq.harvard.edu/people/philip-durbin