We present an approach to the verification of systems for whose description some elements - constants or functions - are underspecified and can be regarded as parameters, and, in particular, describe a method for automatically generating constraints on such parameters under which certain safety conditions are guaranteed to hold. We present an implementation and illustrate its use on several examples.

翻译：我们提出了一种系统验证方法，针对其描述中某些元素（常量或函数）未完全指定且可视为参数的系统，特别描述了一种自动生成此类参数约束的方法，以确保特定安全条件得以满足。我们给出了该方法的实现，并通过多个实例展示了其应用。