Model Checking Timed Systems with Restricted Resources: Algorithms and Complexity

资源有限的定时系统模型检查：算法和复杂性

• 批准号: EP/G069727/1
• 负责人: James Worrell
• 金额: $ 27.04万
• 依托单位: University of Oxford
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2010
• 资助国家: 英国
• 起止时间: 2010 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FG069727%2F1
• 关键词: Model; Checking; Timed; Systems; Restricted

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.

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

项目成果

Mathematical Foundations of Computer Science 2013 - 38th International Symposium, MFCS 2013, Klosterneuburg, Austria, August 26-30, 2013. Proceedings

计算机科学数学基础 2013 - 第 38 届国际研讨会，MFCS 2013，奥地利克洛斯特新堡，2013 年 8 月 26-30 日。

• DOI: 10.1007/978-3-642-40313-2_34
• 发表时间: 2013
• 作者: Felsner S

Reachability Problems - 6th International Workshop, RP 2012, Bordeaux, France, September 17-19, 2012. Proceedings

可达性问题 - 第六届国际研讨会，RP 2012，法国波尔多，2012 年 9 月 17-19 日。会议记录

• DOI: 10.1007/978-3-642-33512-9_6
• 发表时间: 2012
• 作者: Haase C

Foundations of Software Science and Computational Structures

软件科学和计算结构基础

• DOI: 10.1007/978-3-642-19805-2_3
• 发表时间: 2011
• 作者: Levy P

Two Variable vs. Linear Temporal Logic in Model Checking and Games

模型检查和博弈中的二变量与线性时态逻辑

• DOI: 10.2168/lmcs-9(2:4)2013
• 发表时间: 2013
• 期刊: Logical Methods in Computer Science
• 影响因子: 0.6
• 作者: Benedikt M

Automata, Languages, and Programming

自动机、语言和编程

• DOI: 10.1007/978-3-642-39212-2_44
• 发表时间: 2013
• 作者: Christodoulou G