In the observer verification technique, to prove a behavioral property of a program P, first, a program (O) representing the property must be designed. This program listens all the input and output entries of P and emits either an ERROR when the property is violated or an OK when the property is true. The choose between these two approaches depends of the easier way to express the property as a program. Second, the possible presence of ERROR or OK in the model of P || O is verified with model-checking technique.