Runtime and Static Verification of Concurrent Systems

该项目将开发监控系统的技术，以检查它们的执行是否满足自动机或时态逻辑规范指定的属性。将被监测系统建模为随机系统。该项目提出了准确性措施，以表明所需属性被监控的精确度。这项研究将把精度测量作为这类系统的监视器。研究还将开发与底层系统交互的主动监视器，以确保正确性属性，以及从系统检测故障的技术-S外部行为和基于对称约简的模型检测的静态验证技术。这项工作将带来数学上严格和强大的技术，这些技术将提高日益复杂的系统的可靠性。

The project will develop techniques for monitoring systems to check if their executions satisfy a property specified by an automaton or a temporal logic specification. Systems to be monitored are modeled as a stochastic system. The project proposes accuracy measures that denote how accurately the desired property is monitored. The research will implement the accuracy measures as monitors for such systems. The research will also develop active monitors that interact with the underlying system to ensure the correctness properties, as well as techniques for detection of failures from a system?s external behavior and static verification techniques based on model checking employing symmetry based reduction. The work will lead to mathematically rigorous and powerful techniques that will improve the reliability of increasingly complex systems.