CSP Model Checking: New Technology and Techniques

并发性变得越来越重要，这既是为了克服处理器速度的限制，也是为了在日益网络化的世界中允许分布式事务。消息传递被广泛认为是最适合并发的模型。本项目的总体目标是改进基于消息传递的并发性推理技术。进程代数CSP已被广泛用于并发系统的验证，尤其是在计算机安全和硬件设计领域。模型检查器FDR可用于分析在CSP中建模的并发系统。所提出的研究旨在改进执行此类分析的工具和技术。具体而言，工作将集中在三个领域：1.通过改进FDR工具，改进模型检查技术，并借鉴其他工具的经验教训；2.分析参数系统(特别是按部件数量进行参数设置的系统)的技术，以核实系统对所有参数值的正确性；3.改进了对定时系统进行建模和分析的技术。

Concurrency is becoming increasingly important, both to overcome limitations in processor speed, and to allow distributed transactions in an increasingly networked world. Message passing is widely considered to be the most appropriate model for concurrency. The overall aim of this project is to improve techniques for reasoning about concurrency based on message passing. The process algebra CSP has been widely used for the verification of concurrent systems, most notably in the area of computer security and hardware design. The model checker FDR can be used to analyse concurrent systems modelled in CSP.The proposed research aims to improve tools and techniques for performing such analyses. In particular, work will focus in three areas:1. Improvements in model checking technology, via enhancements to the FDR tool, with lessons for other tools;2. Techniques for analysing parameterised systems (in particular systems that are parameterised by the number of components) so as to verify the correctness of the system for all values of the parameter;3.Improved techniques for modelling and analysing timed systems.