4 ms·

Really cool stuff. I have a couple of questions: 1) How do you model the myriad fault types that could possibly occur in distributed systems? 2) Is it possibl

Really cool stuff. I have a couple of questions: 1) How do you model the myriad fault types that could possibly occur in distributed systems? 2) Is it possible to partially model a system? For example, in SOA, the behavior of a service can depend on and be greatly affected by the behavior of other services. Can each service be modeled in isolation with meaningful results? 3) Is the run time of model checking managable? The paper mentioned a few seconds to find bugs, but how long to exhaustively check a model without bugs?

mjb 12y ago
> 1) How do you model the myriad fault types that could possibly occur in distributed systems? You need to think at the right level of abstraction. Are packet loss and reordering really different faults? Are packet loss to a node and the stop failure of that node different faults? The answers depend on your model. Lamport's Fast Paxos model is a good example of how different faults are handled in different levels of models (http://research.microsoft.com/pubs/64624/tr-2005-112.pdf http://research.microsoft.com/pubs/64624/tr-2005-112.pdf). > Is it possible to partially model a system? For example, in SOA, the behavior of a service can depend on and be greatly affected by the behavior of other services. Can each service be modeled in isolation with meaningful results? Yes, there are several powerful techniques for partially modelling systems. One of the most successful is the idea of abstraction (modelling less) and refinement (modelling more). Abstraction and refinement let you move up and down the levels of detail, and "refinement mappings" provide a rigorous tool for ensuring the validity of these moves. "The existence of refinement mappings" (http://research.microsoft.com/en-us/um/people/lamport/pubs/abadi-existence.pdf http://research.microsoft.com/en-us/um/people/lamport/pubs/a...) is the classic paper in this area, and Lamport's earlier "What good is temporal logic?" was one of the first to introduce the idea (http://research.microsoft.com/en-us/um/people/lamport/pubs/what-good.pdf http://research.microsoft.com/en-us/um/people/lamport/pubs/w...). This paper from Van Renesse et al (http://arxiv.org/abs/1309.5671 http://arxiv.org/abs/1309.5671) is a good illustration of the kind of formal things that can be done with refinement. In practice, choosing the level of abstraction to apply these techniques is key to their success, but their flexibility makes it easy to work at any level. Choosing the right one is very application specific, and requires engineering and mathematical judgement. > 3) Is the run time of model checking managable? The paper mentioned a few seconds to find bugs, but how long to exhaustively check a model without bugs? That depends hugely on the complexity of the model. TLC is a very brute-force solution to the problem of model checking (with a few clever optimizations), and run time rises very quickly with model complexity. Model checking is tractable for some very meaningful models.
hayfield 12y ago
I currently have about 3 weeks experience with some different formal verification tools (others will know better), but... 1. While large, the system will have a finite number of desired actions (Read, Write, Send Data, etc), with set paths/transitions between them (think state machines). With each of these things-you-want to happen, there may or may not be corresponding errors. If there are error handling actions, these become further things-you-want-to-happen, and so on. This modelling can be at a fairly high level, so you only need to go 'there may be an error, this is how we may handle it' rather than iterating over every possible error. 2. Each part of a system may be independently modelled, with synchronisation states (waiting for data from another system, etc). A model checker can then generate traces to cover the entire possible set of traces. This means that verification may occur at multiple simultaneous levels - you could model a File System separately to a Network Driver, each of which are separate to an Application making use of these two things. 3. Full formal verification is NP-hard. Model checkers, however, are clever tools and are able to act more intelligently than brute forcing. They can do things like looking at which parts of the state space haven't been covered as thoroughly and covering them better; doing things akin to MC/DC testing; focusing on rare events (a good checker will allow you to customise the types of traces you're interested in). Checkers are also able to output what they have covered along with probabilities of finding certain types of bug. Standard distributions and the Pareto Principle will often hold in terms of guesstimating how long varying levels of confidence will take. Another thing to note is that hardware verification is light years ahead of software verification - there are algorithms that have been used on hardware for decades that are only just being discovered for software verification. You could make a comparison that says a distributed software system is like a modern CPU with various independent parts, and if the CPU can be verified then surely your distributed software system can too.

mjb 12y ago

> 1) How do you model the myriad fault types that could possibly occur in distributed systems? You need to think at the right level of abstraction. Are packet loss and reordering really different faults? Are packet loss to a node and the stop failure of that node different faults? The answers depend on your model. Lamport's Fast Paxos model is a good example of how different faults are handled in different levels of models (http://research.microsoft.com/pubs/64624/tr-2005-112.pdf http://research.microsoft.com/pubs/64624/tr-2005-112.pdf). > Is it possible to partially model a system? For example, in SOA, the behavior of a service can depend on and be greatly affected by the behavior of other services. Can each service be modeled in isolation with meaningful results? Yes, there are several powerful techniques for partially modelling systems. One of the most successful is the idea of abstraction (modelling less) and refinement (modelling more). Abstraction and refinement let you move up and down the levels of detail, and "refinement mappings" provide a rigorous tool for ensuring the validity of these moves. "The existence of refinement mappings" (http://research.microsoft.com/en-us/um/people/lamport/pubs/abadi-existence.pdf http://research.microsoft.com/en-us/um/people/lamport/pubs/a...) is the classic paper in this area, and Lamport's earlier "What good is temporal logic?" was one of the first to introduce the idea (http://research.microsoft.com/en-us/um/people/lamport/pubs/what-good.pdf http://research.microsoft.com/en-us/um/people/lamport/pubs/w...). This paper from Van Renesse et al (http://arxiv.org/abs/1309.5671 http://arxiv.org/abs/1309.5671) is a good illustration of the kind of formal things that can be done with refinement. In practice, choosing the level of abstraction to apply these techniques is key to their success, but their flexibility makes it easy to work at any level. Choosing the right one is very application specific, and requires engineering and mathematical judgement. > 3) Is the run time of model checking managable? The paper mentioned a few seconds to find bugs, but how long to exhaustively check a model without bugs? That depends hugely on the complexity of the model. TLC is a very brute-force solution to the problem of model checking (with a few clever optimizations), and run time rises very quickly with model complexity. Model checking is tractable for some very meaningful models.

hayfield 12y ago

I currently have about 3 weeks experience with some different formal verification tools (others will know better), but... 1. While large, the system will have a finite number of desired actions (Read, Write, Send Data, etc), with set paths/transitions between them (think state machines). With each of these things-you-want to happen, there may or may not be corresponding errors. If there are error handling actions, these become further things-you-want-to-happen, and so on. This modelling can be at a fairly high level, so you only need to go 'there may be an error, this is how we may handle it' rather than iterating over every possible error. 2. Each part of a system may be independently modelled, with synchronisation states (waiting for data from another system, etc). A model checker can then generate traces to cover the entire possible set of traces. This means that verification may occur at multiple simultaneous levels - you could model a File System separately to a Network Driver, each of which are separate to an Application making use of these two things. 3. Full formal verification is NP-hard. Model checkers, however, are clever tools and are able to act more intelligently than brute forcing. They can do things like looking at which parts of the state space haven't been covered as thoroughly and covering them better; doing things akin to MC/DC testing; focusing on rare events (a good checker will allow you to customise the types of traces you're interested in). Checkers are also able to output what they have covered along with probabilities of finding certain types of bug. Standard distributions and the Pareto Principle will often hold in terms of guesstimating how long varying levels of confidence will take. Another thing to note is that hardware verification is light years ahead of software verification - there are algorithms that have been used on hardware for decades that are only just being discovered for software verification. You could make a comparison that says a distributed software system is like a modern CPU with various independent parts, and if the CPU can be verified then surely your distributed software system can too.