Automated quantitative software verification with PRISM

使用 PRISM 自动定量软件验证

基本信息

批准号：
EP/D07956X/2
负责人：
Marta Kwiatkowska
金额：
--
依托单位：
University of Oxford
依托单位国家：
英国
项目类别：
Research Grant
财政年份：
2007
资助国家：
英国
起止时间：
2007 至无数据
项目状态：
已结题

来源：
https://gtr.ukri.org/projects?ref=EP%2FD07956X%2F2
关键词：
Automated quantitative software verification PRISM

项目摘要

Large-scale distributed systems, such as the Internet, broadband wireless at home and mobile phone networks, raise many challenges for the design and engineering of the underlying infrastructure. Such systems crucially depend on robust and efficient communication and coordination protocols that ensure that the overall system is self-organising, timely and energy-efficient, possibly in the presence of unreliable network services and malicious or uncooperative agents. New protocols for distributed coordination are being introduced to manage the limited resources. They increasingly often rely on randomisation, which plays an important role in achieving de-centralisation, and resource awareness, for example adapting to the power level. The combination of randomness and nondeterminism that arises from the scheduling of distributed components introduces complex behaviours that may be difficult to reason about. Assuring correctness, dependability and quality of service of such distributed systems is thus a non-trivial task that necessitates a rigorous approach, and methods for quantitative evaluation of such systems against properties such as ``the probability of battery level dropping below minimum within 5 seconds is guaranteed to be below 0.01 in all critical situations'', are needed. Theoretical foundations of such quantitative analysis have been proposed, with some implemented in software tools and evaluated through case studies. However, no tools and techniques can directly address real programming languages endowed with features such as random choice and timing delays.This proposal is to further develop the foundations for reasoning about probabilistic systems to enable quantitative analysis of real programming languages. The research will involve extending the successful quantitative probabilistic model checker PRISM (www.cs.bham.ac.uk/~dxp/prism/) via predicate abstraction, and develop additional enhancements to the PRISM toolkit in collaboration with the extensive user community. The resulting techniques will also be relevant for other domains in which probabilistic model checking has proved successful, e.g. performance analysis, planning and systems biology.

大规模的分布式系统，例如互联网，在家中的宽带无线和手机网络，为基础基础设施的设计和工程提出了许多挑战。这种系统至关重要的是稳健有效的沟通和协调协议，这些协议确保整体系统是自组织，及时和节能的，可能在不可靠的网络服务以及恶意或不合作的代理下。引入了用于管理有限资源的新的分布式协调协议。他们越来越多地依靠随机化，这在实现偏心化和资源意识中起着重要作用，例如适应力量水平。随机性和非确定性的结合是由分布式组件的调度提出的，引入了可能难以推论的复杂行为。因此，确保此类分布式系统的正确性，可靠性和服务质量是一项不平凡的任务，需要采取严格的方法，以及针对属性进行定量评估的方法，例如``电池电量在5秒内降至最低限度以下的可能性在所有关键情况下，都必须保证低于0.01。已经提出了这种定量分析的理论基础，其中一些在软件工具中实施并通过案例研究进行了评估。但是，没有任何工具和技术可以直接解决具有随机选择和时机延迟等功能的真实编程语言。该提案是进一步开发有关概率系统推理的基础，以实现对真实编程语言的定量分析。该研究将涉及通过谓词抽象扩展成功的定量概率模型检查器PRISM（www.cs.bham.ac.uk/~dxp/prism/），并与广泛的用户社区合作开发了Prism Toolkit的其他增强功能。所得的技术也将与其他概率模型检查成功的其他领域有关，例如绩效分析，计划和系统生物学。

项目成果

期刊论文数量（10）

专著数量（0）

科研奖励数量（0）

会议论文数量（0）

专利数量（0）

Compositional Verification of Probabilistic Systems Using Learning

DOI：
10.1109/qest.2010.24
发表时间：
2010-09
期刊：
2010 Seventh International Conference on the Quantitative Evaluation of Systems
影响因子：
0
作者：
Lu Feng;M. Kwiatkowska;D. Parker
通讯作者：
Lu Feng;M. Kwiatkowska;D. Parker

GRIP: Generic Representatives in PRISM

GRIP：PRISM 中的通用代表

DOI：
10.1109/qest.2007.30
发表时间：
2007
期刊：
影响因子：
0
作者：
Donaldson A
通讯作者：
Donaldson A

Language-Level Symmetry Reduction for Probabilistic Model Checking

DOI：
10.1109/qest.2009.21
发表时间：
2009-09
期刊：
2009 Sixth International Conference on the Quantitative Evaluation of Systems
影响因子：
0
作者：
Alastair F. Donaldson;Alice Miller;D. Parker
通讯作者：
Alastair F. Donaldson;Alice Miller;D. Parker

MULTI-OBJECTIVE MODEL CHECKING OF MARKOV DECISION PROCESSES