Analyzing Real-Time Properties of Concurrent Programs

创建任何类型的无错误软件都是一项众所周知的困难活动。对于实时软件系统来说，它必须及时地与外界交互，困难甚至更大。由于这些系统经常用于安全关键型应用程序，因此它们的正确性尤为重要。这个项目的目标是创建用于自动验证实时程序的各种正确性属性的工具。目标是保证而不是测试这些属性的概率性。因此，正式模型和分析技术的开发是本研究的主要内容。本项目定义了在基于可达性的实时分析中控制状态空间爆炸问题的技术。已经为（非定时）并发性分析定义了几种这种技术。这些技术已经产生了很好的实验结果，例如，在Ada程序中基于petri -net的死锁检测。该项目将现有的并发分析技术扩展到实时分析，并定义了减少实时程序状态空间大小的新技术。该产品是一套用于验证实时程序的软件工具，这些工具将使用程序源代码和底层硬件的时序属性信息，回答有关用高级语言编写的程序的时序和其他查询。

The creation of error-free software of any sort is a notoriously difficult activity. For real-time software systems, which must interact with the world in a timely fashion, the difficulties are even greater. Since these systems are often used in safety-critical applications, it is especially important that they be correct. The objective of this project is to create tools for the automated verification of various correctness properties of real-time programs. The goal is to guarantee rather than to test these properties probabilistically. Therefore, the development of formal models and analysis techniques is a major part of this research. This project defines techniques for controlling the state space explosion problem in reachability-based real-time analysis. Several techniques of this kind have been defined for (untimed) concurrency analysis. These techniques have yielded excellent experimental results, for instance, in the case of Petri-net-based deadlock detection in Ada programs. This project extends existing techniques for concurrency analysis to real-time analysis and defines new techniques for reducing state space size for real-time programs. The product is a set of software tools for the verification of real-time programs These tools would answer timing and other queries about programs written in a high level language, using the program source code and information about the timing properties of the underlying hardware.