Go back to overview

Guest lecture by Dr. Stephan Merz

On 14 Janu­ary 2021, Dr Stephan Merz was talk­ing about the speci­fica­tion lan­guage TLA+ and its tool set with­in the lec­ture series of the Elite Grad­uate Pro­gram "Software Engi­neer­ing". Dr Merz is a re­searcher at Inria in Nan­cy. In his lec­ture, he ex­plained the mod­eling of dis­tributed algo­rithms in TLA+ and the avail­able tools for work­ing with TLA+.

Using TLA+

Dr Merz brief­ly intro­duced the speci­fica­tion lan­guage TLA+ that is based on work done by Leslie Lamport. At first, he pre­sent­ed the basic con­cepts of TLA+ and showed how to model a dis­tributed algo­rithm in­vent­ed by Edsger Dijks­tra in TLA+. Dr Merz con­tinued by demonstrating how to speci­fy safety prop­erties of the algo­rithm in TLA+ and how to prove them with proof assis­tant for TLA+ speci­fica­tions. Af­ter­wards the talk ex­plained the archi­tec­ture of the TLA+ proof sys­tem and how it is cou­pled to the TLA+ Toolbox. Then other inter­esting prop­erties of the algo­rithm were ex­plained and it was shown to the stu­dents of the Elite Grad­uate Pro­gram "Software Engineering"  how the inter­active proof helps to verify them.Dr Merz con­clud­ed with a brief recap of the prop­erties of TLA+ and which tools are avail­able to sup­port the speci­fica­tion engi­neers and the proof engi­neers.

Text: Elite Grad­uate Pro­gram „Software Engi­neer­ing“