A methodology for an incremental, logical specification of real-time systems

A methodology for an incremental, logical specification of real-time systems which is based on an object-oriented extension of a logical specification formalism is presented. Such an object-oriented framework makes available primitives for identifying, partitioning, and structuring the elements of a specification. In such a way it supports a twofold modality of dealing with abstraction, i.e. specialization and decomposition, that provides a guideline for specifications development. In particular, it provides the specifier with the ability to deal with different time granularities within a single specification. That is, it allows the specifier to describe the behavior and the properties of a system and its environment with respect to different time scales, and to switch among them in a suitable way. It also allows an extension of temporal verification and validation of specifications taking into account the incremental development and the resulting layered structure of specifications