t-UNITY - A Formal Framework for Modeling and Reasoning About Timing Constraints in Real-Time Systems

摘要

This paper proposes a timed extension to the UNITY framework, for modeling, specification and reasoning about timing constraints in real-time systems. The UNITY formalism of Chandi and Misra is extended by introducing timing constraints in the definition of safety and liveness properties and in the proof logic. The proposed t-UNITY framework enables specification of both time independent logical properties and real-time properties, without any specific assumptions on scheduling and constraints imposed by implementation environments. The application of t-UNITY formalism to specification and reasoning about real-time systems is illustrated by an example.