权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

Abstraction Discovery and Refinement for Model Checking Partially Ordered State Spaces

模型检查部分有序状态空间的抽象发现和细化

基本信息

批准号：
EP/E026745/1
负责人：
Thomas Melham
金额：
$ 20.49万
依托单位：
University of Oxford
依托单位国家：
英国
项目类别：
Research Grant
财政年份：
2006
资助国家：
英国
起止时间：
2006 至无数据
项目状态：
已结题

来源：
https://gtr.ukri.org/projects?ref=EP%2FE026745%2F1
关键词：
Abstraction Discovery Refinement Model Checking

项目摘要

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.

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