Accession Number : ADA326032

Title :   Symbolic Approximations for Verifying Real-Time Systems.

Descriptive Note : Doctoral thesis,

Corporate Author : STANFORD UNIV CA DEPT OF COMPUTER SCIENCE

Personal Author(s) : Wong-Toi, Howard

PDF Url : ADA326032

Report Date : DEC 1994

Pagination or Media Count : 207

Abstract : Real time systems are appearing in more and more applications where their proper operation is critical, e.g. transport controllers and medical equipment. However they are extremely difficult to design correctly. One approach to this problem is the use of formal description techniques and automatic verification. Unfortunately automatic verification suffers from the state explosion problem even without considering timing information. This thesis proposes a state based approximation scheme as a heuristic for efficient yet accurate verification. We first describe a generic iterative approximation algorithm for checking safety properties of a transition system. Successively more accurate approximations of the reachable states are generated until the specification is provably satisfied or not. The algorithm automatically decides where the analysis needs to be more exact, and uses state partitioning to force the approximations to converge towards a solution. The method is complete for finite state systems. The algorithm is applied to systems with hard real time bounds. State approximations are performed over both timing information and control information. We also approximate the system's transition structure. Case studies include some timing properties of the MAC sublayer of the Ethernet protocol, the tick-tock service protocol, and a timing based communication protocol where the sender's and receiver's clocks advance at variable rates.

Descriptors :   *APPROXIMATION(MATHEMATICS), *COMMUNICATIONS NETWORKS, *HEURISTIC METHODS, *COMMUNICATION AND RADIO SYSTEMS, *COMPUTER PROGRAM VERIFICATION, ALGORITHMS, CONTROL SYSTEMS, COMPUTER COMMUNICATIONS, REAL TIME, THESES, CASE STUDIES, SAFETY, ITERATIONS, AUTOMATIC.

Subject Categories : Numerical Mathematics
      Computer Programming and Software
      Radio Communications

Distribution Statement : APPROVED FOR PUBLIC RELEASE