Analyzing Real-Time Properties of Concurrent Programs

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

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.