Verifying properties of systems with variable timing constraints

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 by F. Jahanian and D.A. Stuart (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