Abstraction Discovery and Refinement for Model Checking Partially Ordered State Spaces

Integrated electronic chips, such as the processor in your laptop, are among the most complex artifacts ever devised by humans. They consist of many millions of interconnected transistors, all working together to run programs. The engineering design of these chips is extremely challenging, and very difficult to get right. Checking that a modern electronics design will produce a chip that does what it's supposed to do occupies up to 80% of the effort in designing a new chip and requires months or years of computer simulation using large banks of computers. Formal verification is an approach to this problem that aims to improve the quality of chip designs using logical reasoning instead of simulation. A mathematical model of the chip design is constructed, and mathematical proofs are done to show that the model describes just those behaviours that we wish the chip itself to have. These models and proofs are usually very complex - far too big for pencil-and-paper mathematics - and specialised computer software is used for them. With formal verification, the functioning of a chip can often be tested and errors discovered far more thoroughly and with much less effort than by simulating it. But there is a problem with this approach too: an accurate and fully detailed mathematical model of a modern chip design would itself be vastly too large and complex to represent and do proofs about, even using state of the art software. An approach to solving this problem is to let the mathematical models we use be abstractions, or simplifications, of the chip designs they represent. Instead of modelling the design in full detail, we represent only its salient features - only those aspects of it which, if got wrong, will produce an error. An abstract model can be much smaller than a fully detailed one, and so be much easier to handle. The difficulty with this method is coming up with an appropriate abstraction. If the abstraction throws away too much information about the design, then it may not say enough about its behaviour to establish that the design does the expected thing. Even worse, such an oversimplification may give a false assurance that the design is right. On the other hand, if we retain too much information about the design, then the model may be too big to be tractable. The problem of finding a good abstraction in general is very difficult and in practice often requires a great deal of human ingenuity and insight. It would be much better to have a way to find good abstractions automatically. One idea is to begin with a fairly crude abstraction, one that simplifies a great deal. If doing proofs with this reveals an error, then we check if there really is an error in the actual design, or if the problem is just an artefact of oversimplification in our model. (There are ways to check this efficiently.) If the error is real, we have found a problem with our design and can repair it. If the error is spurious, then it can give us information that will allow us to refine our abstraction by adding more of the right kind of design detail to it to get a more accurate one. Repeating this process arrives, we hope, at a tractable abstraction that is sufficient for checking our design. This basic idea has many variants and technical subtleties, and there is a rich literature of advanced research on this topic. This project at Oxford will make a contribution to this research by looking at ways of constructing abstractions in a specific modelling and proof framework called Symbolic Trajectory Evaluation (STE). This is one of the most practical formal verification methods; it is used, for example, by Intel. STE provides an especially rich setting for abstractions, but so far most abstractions in STE have been created manually - by experts and with much effort. This research will develop a new abstraction refinement method for STE that will exploit its full potential and make it much easier forengineers to use effectively.