I didn't get any real interest in my office, but I applied TLA+ to a debugging challenge. I described a well-specified system (abbreviated, for instance data was just "DATA", not the actual myriad number of message types that could be sent). The intention was to understand a bug and possibly identify which of three suspected locations it was occurring in. I had enough of the specification for each part implemented:
Two sender/receivers (sending messages back and forth) and a data bus. For some reason, we seemed to be getting bad data (but not consistently). My "debugging" was actually more like "bugging". I took a correct TLA+ spec, and weakened constraints on different parts until I recreated the behavior we were seeing (it was the data bus). But the nice thing was being able to show that the particular bug couldn't happen from the sender/receivers. Their interaction with the data bus were correct (per the specification) and they were the only parts I could directly inspect (as I didn't have the files on how they implemented the data bus itself).
Once I found the right constraints on the data bus to weaken, I recreated the errors we were seeing in the model itself. This led to devising several more test programs that could more reliably produce the error. From there we were able to better communicate the problem with the contractors involved and get things corrected ("proof" that we weren't the problem).
A particularly nice thing was being able to model abstract versions of the system. I didn't need the fine details (what message specifically is being sent, didn't matter). But I also found I needed more details than my first pass and was able to refine the data bus specification (in TLA+) as needed to provide the necessary level of detail and extend it to add new capabilities.
That's awesome! I'm adding this write up to my collection of case studies. You should consider doing a blog post with a mockup problem really similar to illustrate that process with code and specs.
Is also a good introduction. That was enough to make me dangerous. Since work didn’t have an interest in training me, and I had other obligations, that’s all I’ve done so far.
hwayne, who did learntla.com, is getting close to finishing a book on it. You could start with his online tutorial but get the book soon as it's out. Here's his Twitter in case you want to watch for the book release:
Two sender/receivers (sending messages back and forth) and a data bus. For some reason, we seemed to be getting bad data (but not consistently). My "debugging" was actually more like "bugging". I took a correct TLA+ spec, and weakened constraints on different parts until I recreated the behavior we were seeing (it was the data bus). But the nice thing was being able to show that the particular bug couldn't happen from the sender/receivers. Their interaction with the data bus were correct (per the specification) and they were the only parts I could directly inspect (as I didn't have the files on how they implemented the data bus itself).
Once I found the right constraints on the data bus to weaken, I recreated the errors we were seeing in the model itself. This led to devising several more test programs that could more reliably produce the error. From there we were able to better communicate the problem with the contractors involved and get things corrected ("proof" that we weren't the problem).
A particularly nice thing was being able to model abstract versions of the system. I didn't need the fine details (what message specifically is being sent, didn't matter). But I also found I needed more details than my first pass and was able to refine the data bus specification (in TLA+) as needed to provide the necessary level of detail and extend it to add new capabilities.