Checking a functional module of an automation installation

A method for checking a compatibility of a functional module for operation in an installation for process automation, said method comprising:

• receiving via an input interface of the functional module an input signal from the installation, said input signal comprising an operating parameter of the installation,
• producing with the functional module an output signal based on the input signal,
• outputting the output signal to the installation via an output interface of the functional module, said output signal causing a desired behavior of the installation,
• providing for the input interface an input specification as a first-order predicate logic or a quantifier-free predicate logic, which specifies for the input signal all input signal values deemed to be valid for the functional module,
• providing for the output interface an output specification as a first-order predicate logic or a quantifier-free predicate logic, which specifies for the output signal all output signal values supplied by the functional module when the input specification is fulfilled, and
• before the functional module is operated in the installation, checking by an analysis device whether the functional module produces, for an input signal produced by the installation on the input interface in accordance with the input specification, the output signal on the output interface exclusively in accordance with the output specification, and, when at least one output value of the output signal violates the output specification, signaling an incorrect use of the functional module and providing a counterexample that indicates for the input signal the respective input value that yields the output value that violates the output specification and presenting the counterexample to a user to assist the user in detecting incorrect use of the functional module.