4 ms·

I do often employ the simple whiteboard methods described, but I've never found the energy to learn and use stuff like TLA+. What fields do people find them use

I do often employ the simple whiteboard methods described, but I've never found the energy to learn and use stuff like TLA+. What fields do people find them useful in?

01HNNWZ0MV43FF 2y ago
I find my biggest problem is interfacing with apis from complex dependencies I can't control, usually OSes and gui libs. I assume there isn't a ton formal methods can do for that unless I set up a VM I can tightly control?
- buescher 2y ago
  At that point you're probably blowing up your verification/validation space to where it might be intractable , in both a machine and human sense. People have done research work in formal methods all the way down to the assembly level, of course, but could you even write the correctness properties for the software you're describing? Where you can use these methods - think of the part of your program's behavior you can describe with the article's "whiteboard" methods mentioned in the post above - truth tables, decision tables (! TIL), state machines/statecharts. If you can formulate it that way, not only is it easier to reason about and to test, but if you can also work out what would make it correct, you can run it through an automated checker.
Jtsummers 2y ago
My only time using TLA+ "in anger" was on an embedded system. There was a problem in the hardware portion and our boss wanted proof it was the hardware and not our software. He didn't accept any of our evidence that it was a hardware flaw, partially because our tests weren't failing 100% of the time. I used TLA+ and ended up with a handful of traces which we were able to recreate with the hardware and some small programs (remove everything our system actually did, just use the busted data bus) to demonstrate the failure, they always failed instead of failing only 90% of the time (shouldn't have been needed, it was obvious the hardware was broken). The TLA+ model started off being a reasonable fidelity model of the specified hardware bus, and then I started messing with it (in a deliberate fashion, altering state transitions) until I got traces and invariant violations similar to the real-world hardware. I've used Alloy for similar things, but only after the fact not during the investigation and as a way to learn Alloy. I'd use them both again (TLA+ especially) if I could convince people it was worth the time, but it can be difficult to get the time to spend on it at work while also meeting other work obligations. I've used TLA+ for some personal projects involving concurrent and distributed systems (toys, nothing notable just playing). I used TLA+ to demonstrate that my design worked as I intended, and then started writing code based on the model.
- tonyarkles 2y ago
  Yeah, I've done something similar twice for embedded systems. First one was modelling a BLE protocol between a mobile device and a piece of hardware to confirm that the protocol the vendor provided would definitively lose messages in specific circumstances. The second was to model the LoRaWAN protocol as a state machine and prove that the SM model I'd put together couldn't deadlock; the C implementation of it modelled the TLA+ model very closely. I was honestly pretty shocked that after getting the first version of the implementation done there was exactly one bug in it and it was a typo (used the wrong variable somewhere) and not a logic error. Other than that the implementation basically worked perfectly first try and just kept running indefinitely.
chrsig 2y ago
I've been learning Alloy[0], which I think is probably more practical for most software engineers. I'm using it with the goal of documenting and decomposing a legacy system that I've been working with for a number of years. It's more geared towards the static elements of the system, and writing a spec feels quite like writing a relational database schema -- mostly because they're both expressions of relationships. It seems like a pretty natural path to write a spec in alloy before building out some crud interface. I think there's a huge tooling gap though. Alloy, TLA+ and friends all seem to be very jvm/UI centric, really targeting a user who is working in the editors the language ships with. I'd really love to see more tooling to run model checkers in a CI pipeline, or generate stubs and test cases for various languages. If that were in place, I think there would be more stickiness to formal methods. I've started writing a Go parser for alloy, in part to learn it better, in part because I know go and want to write some tooling that I think go would be a good implementation language for. I don't know if anything will come of it, but at least having a parser would allow for things like a formatter or code generator. If I were feeling ambitious, I might try to implement a model checker. [0] https://alloytools.org/ https://alloytools.org/
- photonthug 2y ago
  > tooling to run model checkers in a ci pipeline Helpful to escape the alloy UI: https://github.com/elo-enterprises/docker-alloy-cli https://github.com/elo-enterprises/docker-alloy-cli
  - chrsig 2y ago
    My hero! I looked into what it would take to tackle it from the source code, There were some barriers, like the jars not really being published to maven, but the biggest just being the time & energy investment to pick up java again. I'll definitely be looking into this project and seeing if there's anything I can contribute back.
- rramadass 2y ago
  You might find Viper (Verification Infrastructure for Permission- based Reasoning) from ETH-Zurich useful - https://www.pm.inf.ethz.ch/research/viper.html https://www.pm.inf.ethz.ch/research/viper.html and https://viper.ethz.ch/tutorial/ https://viper.ethz.ch/tutorial/ I came across this when researching/studying Formal Methods but have not yet really sat down and tried it out.

I do often employ the simple whiteboard methods described, but I've never found the energy to learn and use stuff like TLA+. What fields do people find them useful in?

01HNNWZ0MV43FF 2y ago

I find my biggest problem is interfacing with apis from complex dependencies I can't control, usually OSes and gui libs. I assume there isn't a ton formal methods can do for that unless I set up a VM I can tightly control?

buescher 2y ago
At that point you're probably blowing up your verification/validation space to where it might be intractable , in both a machine and human sense. People have done research work in formal methods all the way down to the assembly level, of course, but could you even write the correctness properties for the software you're describing? Where you can use these methods - think of the part of your program's behavior you can describe with the article's "whiteboard" methods mentioned in the post above - truth tables, decision tables (! TIL), state machines/statecharts. If you can formulate it that way, not only is it easier to reason about and to test, but if you can also work out what would make it correct, you can run it through an automated checker.

Jtsummers 2y ago

My only time using TLA+ "in anger" was on an embedded system. There was a problem in the hardware portion and our boss wanted proof it was the hardware and not our software. He didn't accept any of our evidence that it was a hardware flaw, partially because our tests weren't failing 100% of the time. I used TLA+ and ended up with a handful of traces which we were able to recreate with the hardware and some small programs (remove everything our system actually did, just use the busted data bus) to demonstrate the failure, they always failed instead of failing only 90% of the time (shouldn't have been needed, it was obvious the hardware was broken). The TLA+ model started off being a reasonable fidelity model of the specified hardware bus, and then I started messing with it (in a deliberate fashion, altering state transitions) until I got traces and invariant violations similar to the real-world hardware. I've used Alloy for similar things, but only after the fact not during the investigation and as a way to learn Alloy. I'd use them both again (TLA+ especially) if I could convince people it was worth the time, but it can be difficult to get the time to spend on it at work while also meeting other work obligations. I've used TLA+ for some personal projects involving concurrent and distributed systems (toys, nothing notable just playing). I used TLA+ to demonstrate that my design worked as I intended, and then started writing code based on the model.

tonyarkles 2y ago
Yeah, I've done something similar twice for embedded systems. First one was modelling a BLE protocol between a mobile device and a piece of hardware to confirm that the protocol the vendor provided would definitively lose messages in specific circumstances. The second was to model the LoRaWAN protocol as a state machine and prove that the SM model I'd put together couldn't deadlock; the C implementation of it modelled the TLA+ model very closely. I was honestly pretty shocked that after getting the first version of the implementation done there was exactly one bug in it and it was a typo (used the wrong variable somewhere) and not a logic error. Other than that the implementation basically worked perfectly first try and just kept running indefinitely.

chrsig 2y ago

I've been learning Alloy[0], which I think is probably more practical for most software engineers. I'm using it with the goal of documenting and decomposing a legacy system that I've been working with for a number of years. It's more geared towards the static elements of the system, and writing a spec feels quite like writing a relational database schema -- mostly because they're both expressions of relationships. It seems like a pretty natural path to write a spec in alloy before building out some crud interface. I think there's a huge tooling gap though. Alloy, TLA+ and friends all seem to be very jvm/UI centric, really targeting a user who is working in the editors the language ships with. I'd really love to see more tooling to run model checkers in a CI pipeline, or generate stubs and test cases for various languages. If that were in place, I think there would be more stickiness to formal methods. I've started writing a Go parser for alloy, in part to learn it better, in part because I know go and want to write some tooling that I think go would be a good implementation language for. I don't know if anything will come of it, but at least having a parser would allow for things like a formatter or code generator. If I were feeling ambitious, I might try to implement a model checker. [0] https://alloytools.org/ https://alloytools.org/

photonthug 2y ago
> tooling to run model checkers in a ci pipeline Helpful to escape the alloy UI: https://github.com/elo-enterprises/docker-alloy-cli https://github.com/elo-enterprises/docker-alloy-cli
- chrsig 2y ago
  My hero! I looked into what it would take to tackle it from the source code, There were some barriers, like the jars not really being published to maven, but the biggest just being the time & energy investment to pick up java again. I'll definitely be looking into this project and seeing if there's anything I can contribute back.
rramadass 2y ago
You might find Viper (Verification Infrastructure for Permission- based Reasoning) from ETH-Zurich useful - https://www.pm.inf.ethz.ch/research/viper.html https://www.pm.inf.ethz.ch/research/viper.html and https://viper.ethz.ch/tutorial/ https://viper.ethz.ch/tutorial/ I came across this when researching/studying Formal Methods but have not yet really sat down and tried it out.