Since the failures of safety-critical systems may have disastrous consequences,
ensuring their correct behaviour is an important task. To verify that the system
is working without errors, the use of formal methods are practical.
Model-checking is such a method which can be used during the design period to
find faults in the system. During the execution of model-checking the validity
of requirements expressed with temporal logics are examined. Several kinds of
temporal logics exist, my work is based on Linear Temporal Logic.
If a requirement is not valid on a model, we recieve a counterexample as the
result of the model-checking process, with which we can identify faults of the
model. In contrast if the requirement is valid on the model, we do not recieve
any additional information. This presents a problem because the incorrect
translation of an invalid requirement frequently results in a trivially valid
LTL-formula, therefore it is impossible to identify the fault.
Finding the so-called vacuity values of an LTL-formula can help us to
identify these incorrect translations by providing information on which parts of
the formula are unnecessary for the validity of the requirement.
In my work I present a method based on the examination of vacuity values, with
which we can warn the user in case of this type of error. Furthermore I
developed an algorithm to analyise the vacuity of the specification, what I
implemented as part of the PetriDotNet model-checking framework.