Abstraction Discovery and Refinement for Model Checking Partially Ordered State Spaces

集成的电子芯片，如笔记本电脑中的处理器，是人类有史以来设计的最复杂的人工制品之一。它们由数百万个相互连接的晶体管组成，所有这些晶体管都在一起运行程序。这些芯片的工程设计极具挑战性，而且很难做好。检查现代电子设计是否会生产出能够完成预期功能的芯片，占设计新芯片工作的80%，并且需要使用大量计算机进行数月或数年的计算机模拟。形式验证是解决这一问题的一种方法，其目的是使用逻辑推理而不是模拟来提高芯片设计的质量。建立了芯片设计的数学模型，并进行了数学证明，表明该模型描述的正是我们希望芯片本身具有的那些行为。这些模型和证明通常非常复杂--对于纸笔数学来说太大了--而且使用了专门的计算机软件。通过正式的验证，通常可以更彻底地测试芯片的功能，发现错误，而且比模拟要容易得多。但这种方法也有一个问题：现代芯片设计的准确和充分详细的数学模型本身就太大太复杂，无法表示和证明，即使使用最先进的软件也是如此。解决这个问题的一个方法是让我们使用的数学模型成为它们所代表的芯片设计的抽象或简化。我们不是对设计进行详细的建模，而是只表示它的显著特征--只表示如果出错会产生错误的那些方面。抽象模型可以比完全详细的模型小得多，因此更容易处理。这种方法的困难在于提出适当的抽象。如果抽象丢弃了太多关于设计的信息，那么它可能没有充分说明其行为，以确定设计完成了预期的事情。更糟糕的是，这种过于简单化可能会给出错误的保证，即设计是正确的。另一方面，如果我们保留了太多关于设计的信息，那么模型可能太大而不容易处理。一般说来，找到一个好的抽象是非常困难的，在实践中往往需要大量的人类创造力和洞察力。如果有一种方法自动找到好的抽象，那会好得多。一种想法是从一个相当粗糙的抽象开始，一个可以大大简化的抽象。如果对此进行证明发现有错误，则我们检查实际设计中是否真的存在错误，或者问题是否只是模型中过于简化的人工制品。(有一些方法可以有效地检查这一点。)如果错误是真实的，我们已经发现了我们设计的问题，并可以修复它。如果错误是虚假的，那么它可以给我们提供信息，允许我们通过添加更多正确的设计细节来精炼我们的抽象，以获得更准确的设计细节。重复这个过程，我们希望，得到一个容易处理的抽象，足以检查我们的设计。这个基本想法有许多变体和技术微妙之处，并且有关于这个主题的丰富的高级研究文献。牛津大学的这个项目将通过寻找在称为符号轨迹评估(STE)的特定建模和证明框架中构建抽象的方法来为这项研究做出贡献。这是最实用的正式验证方法之一；例如，英特尔使用了这种方法。STE为抽象提供了特别丰富的设置，但到目前为止，STE中的大多数抽象都是由专家花费大量精力手动创建的。这项研究将为STE开发一种新的抽象求精方法，充分发挥其潜力，使工程师更容易有效地使用它。

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.