3 ms·

Maybe this is just my ignorance speaking, but I think that using formal methods would take a lot of time; more than the projects I am working on are worth. Als

Maybe this is just my ignorance speaking, but I think that using formal methods would take a lot of time; more than the projects I am working on are worth. Also, I don't know how to do it. I mean, at school we had some examples, but those were for math-like stuff (how to verify that the algorithm calculating the square root actually calculates the square root), but I wouldn't know how to apply that to programs that are mostly reading something from database and displaying it on a web page. Now that I googled a bit, I found a paper https://arxiv.org/abs/1809.03162 https://arxiv.org/abs/1809.03162 claiming that "Tools for formal verification of Java programs are in generally poor shape, and do not support recent versions of Java". That would explain why smarter people around me are also not using them. Give me a tool that is easy to install and works reliably, and I will be happy to learn a new thing.

Jtsummers 6y ago
I think you've hit the problem of "why it isn't adopted" really well. Most people seem to have learned formal methods as "prove this source code does exactly what it should based on the spec", but formal methods don't have to apply at just that level. Formal methods can be applied at the specification level, instead. This can be much simpler as you get to ignore a lot of extraneous details. This is also important because many real-world problems are not because the code is implemented correctly, but because the code implements a bad specification (the spec doesn't do what they think it does). Using something like TLA+ or state diagrams or other things which can be executed (in a sense), which are formal representations of the specification, you can find the issues in the specification before you even touch the code. I've also used it as a way to "debug" by taking the ideal, creating the spec and showing it does work correctly, then weakening the constraints in the model until it behaved like the implementation, which gave an idea of where to check in the implementation (which found the problem, but was hard to debug because it was an embedded system). A (more) concrete example: We had an embedded system with multiple nodes running internally and concurrently that communicated via a shared memory system. You may have already guessed that this could lead to race conditions, and that's what we found. But in trying to sell TLA+ to a colleague, I showed a model of how they were using the system for a part that was constantly giving them errors. We were able to create a much simpler model than the code (which had become several thousand lines in each of two nodes). The model was maybe 100 lines long and focused strictly on how they communicated. We dropped out the message contents (irrelevant) and only modeled the size (variable, but we simplified to 1-10 or something like that) and the buffer size (for the model this was configurable) and the list pointing to where in the buffer messages started (list length was configurable), and a few other details. In making the specification it became clear where the problem was and we didn't even have to run the model checker. If they'd started with modeling that specification more formally (what they had was all prose and tens of pages long in two specification documents), they would've saved months of headaches cleaning up the numerous issues with it.

Jtsummers 6y ago

I think you've hit the problem of "why it isn't adopted" really well. Most people seem to have learned formal methods as "prove this source code does exactly what it should based on the spec", but formal methods don't have to apply at just that level. Formal methods can be applied at the specification level, instead. This can be much simpler as you get to ignore a lot of extraneous details. This is also important because many real-world problems are not because the code is implemented correctly, but because the code implements a bad specification (the spec doesn't do what they think it does). Using something like TLA+ or state diagrams or other things which can be executed (in a sense), which are formal representations of the specification, you can find the issues in the specification before you even touch the code. I've also used it as a way to "debug" by taking the ideal, creating the spec and showing it does work correctly, then weakening the constraints in the model until it behaved like the implementation, which gave an idea of where to check in the implementation (which found the problem, but was hard to debug because it was an embedded system). A (more) concrete example: We had an embedded system with multiple nodes running internally and concurrently that communicated via a shared memory system. You may have already guessed that this could lead to race conditions, and that's what we found. But in trying to sell TLA+ to a colleague, I showed a model of how they were using the system for a part that was constantly giving them errors. We were able to create a much simpler model than the code (which had become several thousand lines in each of two nodes). The model was maybe 100 lines long and focused strictly on how they communicated. We dropped out the message contents (irrelevant) and only modeled the size (variable, but we simplified to 1-10 or something like that) and the buffer size (for the model this was configurable) and the list pointing to where in the buffer messages started (list length was configurable), and a few other details. In making the specification it became clear where the problem was and we didn't even have to run the model checker. If they'd started with modeling that specification more formally (what they had was all prose and tens of pages long in two specification documents), they would've saved months of headaches cleaning up the numerous issues with it.