Abstraction Discovery and Refinement for Model Checking Partially Ordered State Spaces

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