Accession Number : ADA462244


Title :   A Benchmark for Comparing Different Approaches for Specifying and Verifying Real-Time Systems


Descriptive Note : Research paper


Corporate Author : NAVAL RESEARCH LAB WASHINGTON DC


Personal Author(s) : Heitmeyer, C L ; Labaw, B G ; Jeffords, R D


Full Text : https://apps.dtic.mil/dtic/tr/fulltext/u2/a462244.pdf


Report Date : Jan 1993


Pagination or Media Count : 5


Abstract : 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.


Descriptors :   *SOFTWARE ENGINEERING , *REAL TIME , *SYSTEMS ANALYSIS , *COMPUTER PROGRAM VERIFICATION , *SPECIFICATIONS , TIME INTERVALS , AUTOMATIC , THEOREMS , CROSSINGS , RAILROADS , PROBLEM SOLVING , LOGIC , SAFETY


Subject Categories : Operations Research
      Computer Programming and Software


Distribution Statement : APPROVED FOR PUBLIC RELEASE