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.