5 ms·

For those who have used modeling tools like TLA+ and Alloy in industry -- could you give an example of at what point(s) in the development process you used the

by gklitt 8y ago

For those who have used modeling tools like TLA+ and Alloy in industry -- could you give an example of at what point(s) in the development process you used the tool and how long it took? I'm intrigued, but having trouble visualizing how even lightweight formal methods can fit into an agile development process at a startup building a web application.

segmondy 8y ago
You won't use this to model your web application, but the core logic. Usually it's really important that this core logic doesn't break. Imagine something like twitter, why would you model it? Once you start thinking of having N servers, and you have to deal with caches, and consistence of message then it might make sense to model it to make sure that tweets get to the right users, are not lost and duplicates don't happen. You are not exactly modeling the web or mobile application but the "system". At the end of the day, your goal is a logically sound system. So figure out what will make your web application non-logically, if it's going to provide a terrible experience and it's hard to reason, then you might want to model it.
- heavenlyblue 8y ago
  OK, but could you model Twitter in TLA+ and then would TLA+ be able to find inconsistencies in the model given that you relax certain assumptions? Can TLA+ direct you to which of the caches is being incorrectly invalidated given that you have provided that 10% of the servers online are still using the old version of the software? That seems interesting, but haven't yet played with TLA+ enough to know that.
  - pron 8y ago
    You can't know which of the caches is incorrectly validated, but if you specify the behavior of both new and old versions, you could check to see if mixing them could cause problems. But the more elaborate the specification, the harder it may be to answer the question. Using tools like Coq, you essentially need to write the proof (say, of the claim that mixing the versions could cause no issue with data consistency) yourself. With TLA+ you can do the same, but also have the option of letting the model checker check the theorem automatically for you, but the more elaborate the spec, the longer that would take. This is why you need to learn to specify at a level of detail that's right for answering the questions you want answered -- no lower (higher abstraction), or there may not be sufficient detail to answer them, and no lower, or answering may take a long time. Sometimes you'll find that you're specifying the same system at several levels of detail. One of the cool things in TLA+ is that you can check that the different levels are indeed related (could be a description of the same system at different levels).
    - heavenlyblue 8y ago
      On a more practical side of things - how do you mix your application code with TLA+? E.G. Do you have a "proof" project and a the code in different directories with comments in the TLA+ pointing to the files in the actual code? It would be incredibly nice if I could put TLA+ proofs in the comments next to every function or module I am working with and then choosing which of them to be proved. But that seems to be way beyond what the toolset allows you to do.
      - pron 8y ago
        1. Writing formal proofs in TLA+ (or in any other proof assistant) is almost always a waste of time. If the proof is very easy, you can certainly do it, but then you don't need to unless it's a strict requirement or an academic project whose entire purpose is to show that a formal proof is possible rather than some functional correctness requirement. And if the proof is not easy, then there are better methods, like using TLA+'s model checker. 2. Putting references to the TLA+ spec in the code could be nice and useful. 3. You should realize that the benefit from a powerful tool like TLA+ comes when it helps you reason about things that are hard for you to do, and those are hardly ever at the code level. So while using a code-level tool like Why3 to prove some routine is cool, it is hardly ever done in practice, because that's hardly every where the problems you need help with are. Those are usually found in complex interactions between machines, or your program and the user etc.. So often TLA+ is most useful when the specification is so far above the code level that a direct link is not entirely useful. Having said that, you could use TLA+ to actually prove at the code level by compiling your code to TLA+, as has been done with Isabelle or Coq. This has been done for TLA+ with C and Java, but in practice, code-level verification is not where you'll get the most bang for your buck.
marco_salvatori 8y ago
You might create a TLA model during the initial specification process to assist you in thinking through your problem. You would then update the model going forward as your understanding of the domain improved and as system requirements changed. However, you could write a specification for an existing system as well. Any processing where the complexity seems greater than ones reasoning ability or that needs assurance guarantees, could signal the need for a high level description to guide engineering efforts. An initial model might take 4 hours to put in place. The time would be spent thinking through how best to abstract the modeled process and its logical properties, slowly building up a more and more complete set of events, and checking the model by running it as one goes. With an initial model, additional hours would probably be spent here and there adding enhancements and finding ways to do things better, just like one would do with regular code. The model would effectively exist over the lifetime of a corresponding code artifact and guide work on the artifact. For a standard web application that mostly does reads and writes to a database, there usually wouldn't be any need for a tool like TLA to help you reason. A general use case for TLA is describing systems where there are multiple processes or threads coordinating on some sort of shared state.There would be indeterminacy in the order in which events happen. There could be the possibility of failure and the need to handle it gracefully.
- fulafel 8y ago
  Web applications can be surprisingly complicated distributed systems, when you take into account.. - the JS frontend that communicates with AJAX and/or WebSockets IPC with the backend - the backend may actually be a bunch of microservices - the fact that there are many concurrent frontends (users) - messages from frontends may end up reordered/dropped/rerouted on their way to different backend ipc channels (microservices or replicated backend) - the frontends are untrusted (the user or browser may tamper with your code running there) - the backend server is also often replicated / sharded - there are caches (think Redis) that the backends share in addition to the main DB. - load balancers, high-availability reverse proxies with various failover propreties, etc - various caching behaviours that are only partly under your control (browser-side content caching, DNS, etc) - all of the above are interconnected over unreliable channels - there are secrets and security involved so functional assurance ("pressing button X always makes function Y happen") doesn't tell you enough (I have no TLA+ experience so can't say how one would use it with a web app, though).

by gklitt 8y ago

segmondy 8y ago

You won't use this to model your web application, but the core logic. Usually it's really important that this core logic doesn't break. Imagine something like twitter, why would you model it? Once you start thinking of having N servers, and you have to deal with caches, and consistence of message then it might make sense to model it to make sure that tweets get to the right users, are not lost and duplicates don't happen. You are not exactly modeling the web or mobile application but the "system". At the end of the day, your goal is a logically sound system. So figure out what will make your web application non-logically, if it's going to provide a terrible experience and it's hard to reason, then you might want to model it.

heavenlyblue 8y ago
OK, but could you model Twitter in TLA+ and then would TLA+ be able to find inconsistencies in the model given that you relax certain assumptions? Can TLA+ direct you to which of the caches is being incorrectly invalidated given that you have provided that 10% of the servers online are still using the old version of the software? That seems interesting, but haven't yet played with TLA+ enough to know that.
- pron 8y ago
  You can't know which of the caches is incorrectly validated, but if you specify the behavior of both new and old versions, you could check to see if mixing them could cause problems. But the more elaborate the specification, the harder it may be to answer the question. Using tools like Coq, you essentially need to write the proof (say, of the claim that mixing the versions could cause no issue with data consistency) yourself. With TLA+ you can do the same, but also have the option of letting the model checker check the theorem automatically for you, but the more elaborate the spec, the longer that would take. This is why you need to learn to specify at a level of detail that's right for answering the questions you want answered -- no lower (higher abstraction), or there may not be sufficient detail to answer them, and no lower, or answering may take a long time. Sometimes you'll find that you're specifying the same system at several levels of detail. One of the cool things in TLA+ is that you can check that the different levels are indeed related (could be a description of the same system at different levels).
  - heavenlyblue 8y ago
    On a more practical side of things - how do you mix your application code with TLA+? E.G. Do you have a "proof" project and a the code in different directories with comments in the TLA+ pointing to the files in the actual code? It would be incredibly nice if I could put TLA+ proofs in the comments next to every function or module I am working with and then choosing which of them to be proved. But that seems to be way beyond what the toolset allows you to do.
    - pron 8y ago
      1. Writing formal proofs in TLA+ (or in any other proof assistant) is almost always a waste of time. If the proof is very easy, you can certainly do it, but then you don't need to unless it's a strict requirement or an academic project whose entire purpose is to show that a formal proof is possible rather than some functional correctness requirement. And if the proof is not easy, then there are better methods, like using TLA+'s model checker. 2. Putting references to the TLA+ spec in the code could be nice and useful. 3. You should realize that the benefit from a powerful tool like TLA+ comes when it helps you reason about things that are hard for you to do, and those are hardly ever at the code level. So while using a code-level tool like Why3 to prove some routine is cool, it is hardly ever done in practice, because that's hardly every where the problems you need help with are. Those are usually found in complex interactions between machines, or your program and the user etc.. So often TLA+ is most useful when the specification is so far above the code level that a direct link is not entirely useful. Having said that, you could use TLA+ to actually prove at the code level by compiling your code to TLA+, as has been done with Isabelle or Coq. This has been done for TLA+ with C and Java, but in practice, code-level verification is not where you'll get the most bang for your buck.

marco_salvatori 8y ago

You might create a TLA model during the initial specification process to assist you in thinking through your problem. You would then update the model going forward as your understanding of the domain improved and as system requirements changed. However, you could write a specification for an existing system as well. Any processing where the complexity seems greater than ones reasoning ability or that needs assurance guarantees, could signal the need for a high level description to guide engineering efforts. An initial model might take 4 hours to put in place. The time would be spent thinking through how best to abstract the modeled process and its logical properties, slowly building up a more and more complete set of events, and checking the model by running it as one goes. With an initial model, additional hours would probably be spent here and there adding enhancements and finding ways to do things better, just like one would do with regular code. The model would effectively exist over the lifetime of a corresponding code artifact and guide work on the artifact. For a standard web application that mostly does reads and writes to a database, there usually wouldn't be any need for a tool like TLA to help you reason. A general use case for TLA is describing systems where there are multiple processes or threads coordinating on some sort of shared state.There would be indeterminacy in the order in which events happen. There could be the possibility of failure and the need to handle it gracefully.

fulafel 8y ago
Web applications can be surprisingly complicated distributed systems, when you take into account.. - the JS frontend that communicates with AJAX and/or WebSockets IPC with the backend - the backend may actually be a bunch of microservices - the fact that there are many concurrent frontends (users) - messages from frontends may end up reordered/dropped/rerouted on their way to different backend ipc channels (microservices or replicated backend) - the frontends are untrusted (the user or browser may tamper with your code running there) - the backend server is also often replicated / sharded - there are caches (think Redis) that the backends share in addition to the main DB. - load balancers, high-availability reverse proxies with various failover propreties, etc - various caching behaviours that are only partly under your control (browser-side content caching, DNS, etc) - all of the above are interconnected over unreliable channels - there are secrets and security involved so functional assurance ("pressing button X always makes function Y happen") doesn't tell you enough (I have no TLA+ experience so can't say how one would use it with a web app, though).