|
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. |