Experiments with parametric verification of real-time systems

The paper addresses experiments with parametric verification of real-time systems based on model-checking of models of these systems. We apply a model checking a algorithm that implements the partition refinement approach. The models itself are based on the timed automata model of Alur and Dill (1994). The model specification language XTG enables the specification of constant parameters, which are given a valuation during the verification process. The outcome of the verification is presented as relations over the parameters within the specification. This feature adds a substantial power to the model-checking approach to verification. We demonstrate the usefulness of parametric verification by means of two small examples