| 摘要 |
A method is specified for determining the quality of a quantity of properties describing a machine, including a step for determining the existence of at least one sub-quantity of interrelated properties (P0, P1, . . . Pn) of the form Pi=(forall t. A<SUB>i</SUB>(t)=>Z<SUB>i</SUB>(t)), wherein A<SUB>i</SUB>(t) present an initial state and Z<SUB>i</SUB>(t) a target state for a corresponding property and at least one initial state A<SUB>i </SUB>is dependant on internal signals and including a step for checking whether at least one aspect of the input/output behaviour of the machine described by the properties, which cannot be derived from an individual property P<SUB>i</SUB>, is described to such an accurate extent that one property Q exists, which represents this aspect without being dependant on the internal signals. The procedure is capable of providing a measurement and can particularly be used in the verification and specification of circuits.
|
