Dealing with Different Time Granularities in Formal Specifications of Real-Time Systems

The article presents a formalization of the notion of time granularity within a logical language for specifying real-time systems. It provides the specifier with the ability of dealing 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. The extended logical formalism is then embedded in an object oriented structure that enhances both the expressive power and the executability of the specification language. With regard to expressiveness, it enables one to subdivide a single specification of the system and its environment into different part and to provide a number of specifications of them at different levels of abstraction, each one referring to a different time granularity. With regard to executability, it allows one to verify the consistency and the adequacy of specifications at each step of their incremental development. It also suggests an enlargement of the notions of verification and validation that takes into account the stratified structure of the object oriented specifications.