Model Checking Timed Systems with Restricted Resources: Algorithms and Complexity

计算机软件和硬件系统是人类创造的最复杂的工件之一，因此它们经常因设计错误而遭受代价高昂或灾难性的故障也就不足为奇了。2002年，美国国家标准与技术研究所的一项研究估计，仅软件故障一项，每年就给美国经济造成600亿美元的损失。在这种背景下，人们越来越认识到，模型检查-一种正式验证软件和硬件系统正确性的方法-在满足生产正确运行的系统的挑战方面发挥着重要作用。英特尔、朗讯、微软、摩托罗拉和NASA等许多公司已经将模型检查作为其质量保证过程的一部分。简而言之，模型检测就是构造一个给定系统的形式化模型，然后自动或半自动地检查该模型是否满足给定的形式化规范，这一任务的主要挑战之一就是所谓的状态爆炸问题。例如，一个10兆字节的高速缓存有10 ^（20，000，000）个状态。状态爆炸问题所带来的挑战刺激了大量技术的发展，这些技术融合了自动机理论、人工智能、组合优化、博弈论、图论和数理逻辑的思想。2007年，Clarke、Emerson和Sifakis因其在模型检验方面的开创性工作而获得图灵奖（计算机科学界的诺贝尔奖）。在这个项目中，我们特别关注实时系统，如硬件、控制器和嵌入式系统。这种系统的校正器可接受性可以取决于实时约束，例如，防抱死制动系统的响应时间或视频传输的延迟。状态爆炸问题对于实时系统来说尤其严重--实际上它们本质上是无限状态系统。因此，在实时模型检查中，必须非常小心地设计建模和规范形式主义。显然，这些微小的变化可以导致drasticchanges模型checking.The项目的目的是确定建模和规范的形式主义，可以表达上述类型的系统需求，也允许模型检查算法，具有合理的复杂性。该项目的一个重要成果将是用于模型检查实时系统的算法和工具。这种算法将采用新的组合和自动机理论的想法，并将使用符号技术，允许穷举搜索无限状态空间。该项目的另一个成果将是加强对使用时序逻辑推理实时行为的理解，建立在离散时间系统的时序逻辑的高度成功使用的基础上。

Computer software and hardware systems are among the most complexartifacts created by humans, thus it is not surprising that they often suffercostly or catastrophic failures due to errors in design. In 2002 a study by the US National Institute of Standard and Technology estimated that software failures alone cost the US economy 60 billion dollars per year. Against this background it is increasingly recognized that model checking---an approach to formally verifying the correctness of software and hardware systems---has an important role to play in meeting the challenge of producing correctly functioning systems. Intel, Lucent, Microsoft, Motorola, and NASA, among many others, already use model checking as part of their quality assurance process. In a nutshell, model checking involves constructing a mathematicalmodel of a given system and then checking, automatically orsemi-automatically, that the model meets a given formal specification.One of the main challenges of this task is the so-called stateexplosion problem. For example, a 10 mega-byte cache has10^(20,000,000) states. The challenge presented by the stateexplosion problem has spurred the development of a rich body oftechniques, incorporating ideas from automata theory, artificialintelligence, combinatorial optimization, game theory, graph theoryand mathematical logic. In 2007 Clarke, Emerson and Sifakis wereawarded a Turing award (the Computer Science equivalent of a Nobleprize) for their pioneering work in model checking.In this project we are concerned in particular with real-time systems,such as hardware, controllers and embedded systems. The correctnessor acceptability of such systems can depend on real-time constraints,e.g., the response time of an anti-lock braking system or the latencyin video transmission. The state explosion problem is particularlyacute for real-time systems--indeed they are essentiallyinfinite-state systems. As a consequence, in real-time model checkingone must take great care in designing the modelling and specificationformalisms. Apparently minor variations in these can lead to drasticchanges in the tractability of model checking.The aim of this project is to identify modelling and specification formalisms that can express the type of system requirements described above, that also permit model checking algorithms that have reasonable complexity. An important outcome of this project will be algorithms and tools for modelchecking real-time systems. Such algorithms will employ novel combinatorial and automata-theoretic ideas, and will use symbolic techniques to permit exhaustive search of infinite state spaces. Another outcome of this project will be to enhance understanding of the use of temporal logics for reasoning about real-time behaviours, building on the highly successful use of temporal logics for discrete-time systems.