Bild 6 zeigt beispielhaft den Ablauf einer Verifikation mit der vorgestellten Methode. Zur Vereinfachung wird in diesem Bild die Verifikation anhand des funktionsspezifischen Verifikationsmodells gezeigt. Jede Nachricht durchläuft jedoch zunächst das busspezifische Verifikationsmodell. Als Eingabe für die Verifikation dient hier eine Busaufzeichnung (Trace), die eine Abfolge von MOST-Nachrichten enthält. In dieser Aufzeichnung ist das Verhalten des MOST-Funktionsblocks AuxiliaryInput protokolliert. Zu Beginn der Nachrichtensequenz synchronisiert sich das Verifikationsmodell mit dem Trace, indem es in den Startzustand springt. Anschließend dient der Trace als Eingabe für das Verifikationsmodell, indem zeilenweise jede MOST-Nachricht in das Modell eingelesen wird. Falls eine eingelesene MOST-Nachricht vom Verifikationsmodell verarbeitet werden kann – die Nachricht also einen Zustandsübergang auslöst – so entspricht die Nachricht dem spezifizierten Verhalten des Funktionsblocks und das Modell wechselt in den Zielzustand der Transition. Falls eine MOST-Nachricht keinen Zustandsübergang auslöst, entspricht das im Trace protokollierte Verhalten nicht dem spezifizierten Verhalten. Das bedeutet, dass sich der Funktionsblock, dessen Verhalten in dem betrachteten Trace aufgezeichnet wurde, nicht konform zur Spezifikation verhält. In dem in Bild 6 dargestellten Beispiel ist das bei der letzten MOST-Nachricht aus dem Trace der Fall. Nach der in Bild 2 spezifizierten Sequenz antwortet der Funktionsblock AuxiliaryInput auf die eingehende Nachricht SouceActivity_StartResult, die den Parameter Activity=‘On‘ enthält, mit der Nachricht SourceActivity_Result und Parameter Activity=‘On‘.
Die nächste Nachricht im hier betrachteten Trace, SourceActivity_Result, enthält allerdings den Parameter Activity=‘Off‘. Diese Nachricht kann im aktuellen Zustand VerifikationState_2 des funktionsspezifischen Verifikationsmodells nicht verarbeitet werden, da sie aufgrund des falschen Parameters keine Transition auslöst. Das Verifikationsmodell geht daher in den Fehlerzustand (OutOfSync) über und gibt die Fehlermeldung „Unexpected message received“ aus. In einer anschließenden Analyse kann für den Fehler die entsprechende Stelle im Modell markiert und der Pfad, der zu diesem Fehler geführt hat, ausgegeben werden.