Trace Algebra for Automatic Verification of Real-Time Concurrent Systems
Abstract
Verification methodologies for real-time systems can be classified according to whether they are based on a continuous time model or a discrete time model. Continuous time often provides a more accurate model of physical reality, while discrete time can be more efficient to implement in an automatic verifier based on state exploration techniques. Choosing a model appears to require a compromise between efficiency and accuracy. We avoid this compromise by constructing discrete time models that are conservative approximations of appropriate continuous time models. Thus, if a system is verified to be correct in discrete time, then it is guaranteed to also be correct in continuous time. We also show that models with explicit simultaneity can be conservatively approximated by models with interleaving semantics.
Document Details
- Document Type
- Technical Report
- Publication Date
- Aug 01, 1992
- Accession Number
- ADA256199
Entities
People
- Jerry R. Burch
Organizations
- Carnegie Mellon University