Automatic abstractions of real-time specifications

This paper explores the automatic generation of abstractions of real-time specifications. Abstractions of formal specifications hide certain details while preserving other essential aspects of system behavior. Abstractions are useful in the context of model-checking because the state-space explosion problem often prohibits model-checking of the full specification. Abstractions are commonly used to develop reduced models, but the abstractions are often generated in ad hoc, informal and not automated ways. As a consequence, the reduced models may be incorrect-that as, they may not accurately capture the behavior of the original specification. The approach described here uses dependency information to automatically generate mathematically sound abstractions for real-time specifications. In addition, timing information is incorporated to further reduce the model. The technique is illustrated by an example which yields a 26% reduction in the time required to generate the state-space representing equivalent behavior to the original specification