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 f these systems. We apply a model checking algorithm that implements the partition refinement approach. The models itself are based on the timed automata model of Alur and Dill [3]. 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 usefullness of parametric verification by means of two small examples.