Benchmark for Comparing Different Approaches for Specifying and Verifying Real-Time Systems.

摘要

To be considered correct or useful, real-time systems must deliver results within specified time intervals, either without exception or with high probability. Recently, a large number of formal methods have been invented for specifying and verifying real-time systems. It has been suggested that these formal methods need to be tested out on actual real-time systems. Such testing will allow the scalability of the methods to be assessed and also will uncover new problems requiring a formal solution. However, before these methods can be productively applied to industrial systems, greater understanding is needed about how they compare (e.g., what classes of problems they are designed to solve, the availability of mechanical support, etc.). To provide insight into the utility of different methods for solving real-time problems, the authors have developed a generic version of a real-time railroad crossing system. Their plan is to use this example as a benchmark for comparing different formalisms. In this paper, the authors define the problem, describe three classes of formalisms that can be applied, and summarize efforts currently in progress to specify the system of interest and prove properties about its behavior.