Verifying properties of systems with variable timing constraints

Abstract

A method is presented for the specification and verification of real-time systems in which some of the timing constraints are specified as variables. These variables can be viewed as parameters of the system under consideration. A set of inequalities restricts the range of values that a variable can be assigned relative to other variables (parameters) of the system. The proposed method extends an earlier work (F. Jahanian and D. A. Stuart, ibid., pp. 12-21, 1988) for verifying properties of systems expressed in the Modechart language where timing constraints were specified as integer constants. Also presented are results on the undecidability of verifying properties of systems.