Verifying of interface assertions for infinite state Mealy machines

• Interface assertions specifying the interface behavior of state machines.
• Verification of interface assertions for state machines by generalized invariants.
• Proof of liveness properties.

This paper aims at techniques and methods for the verification of logical assertions about the interface behavior of generalized I/O-state machines. The interface behavior of such machines is specified by interface assertions formulated in predicate logic. Interface assertions specify the interface behavior of state machines in terms of the streams of messages produced via their input and output channels. The verification of interface assertions for state machines is carried out with the help of generalized invariants. Such invariants are proved for state machines in terms of stable assertions. Nontrivial liveness properties such as fairness lead to specifications and also to state machines defining sets of computations that specify sets of output streams that are not limit closed. Elementary examples for such cases are described and the implied complications are analyzed. Furthermore, verification methods are provided for these cases and demonstrated by small examples.