Automated Methods for Verification of Concurrent Software Systems

CCR 9988884标题：并发系统分析和验证的自动化方法PI：A.Prasad Sista摘要：该项目研究了基于时态逻辑模型检测的各种并发和分布式系统的自动化分析方法，包括电子商务等基于因特网的应用的安全验证。将研究使用基于对称性和偏序的混合技术来抑制状态爆炸和检查安全性和活动性。该项目还考虑了由任意数量的进程组成的系统的验证工作。将探索对具有不同网络拓扑的此类系统进行验证。作为这项工作的一部分，将开发基于归纳的技术以及算法技术。安全验证将考虑不同的安全属性、入侵者和协议模型。该项目强调基础研究和实验工作，以实现和应用于真实世界的问题的形式。

CCR 9988884 Title: Automated Methods in the Analysis and Verification of Concurrent Systems PI: A. Prasad SistlaAbstract: The project investigates various methods, based on temporal logic model-checking, for automatedanalysis of concurrent and distributed systems includingsecurity verification of Internet based applications suchas e-commerce.Hybrid techniques, employing symmetry and partial order basedmethods, will be investigated for containingthe state explosion and for checking both safety and liveness properties.The project also considers work on verification of systems composed of arbitrary number of processes. Verification of such systemswith different network topologies will be explored. As part of this work, induction based techniques as well asalgorithmic techniques will be developed. The security verification willconsider different security properties, intruder and protocol models.The project emphasizes both basic research as well as experimental work in the form of implementationand application to real-world problems.