Für die Generierung dieser Verifikationsmodelle wird der Ansatz verfolgt, das busspezifische Verhalten getrennt von dem funktionsspezifischen Verhalten zu generieren und damit auch zu verifizieren. Das funktionsspezifische Modell beinhaltet dabei die logischen Abläufe der Funktion und abstrahiert von der verwendeten Technologie. Das busspezifische Verifikationsmodell hingegen wird aus dem Funktionskatalog generiert und ist in der Lage, die Einhaltung des MOST-Protokolls zu überprüfen. Für jede im Funktionskatalog beschriebene Funktion wird darin ein Zustand generiert, der alle möglichen Operationen (z.B. Set, Get, Notification) als Transitionen besitzt. Der Ausschnitt aus dem busspezifischen Verifikationsmodell in Bild 4 zeigt als Beispiel dafür die Funk-tion DeckStatusAuxIn. Zusätzlich behält dieses busspezifische Verifikationsmodell den Überblick über alle notifizierten Funktionen und verifiziert bei jeder Statusänderung des Funktionsblocks, ob jeder registrierte Teilnehmer eine Aktualisierung erhält.
Bild 5 zeigt das funktionsspezifische Verifikationsmodell nach der Transformation aus dem Referenzmodell. Das funktionsspezifische Verifikationsmodell wird dabei vollständig auf Grundlage der im Referenzmodell enthaltenen Informationen generiert. Die zusätzlich erstellten Verifikationszustände (z.B. VerifikationState_1 in Bild 5) werden benötigt, um nicht nur die vom Controller gesendeten Stimuli-Nachrichten, sondern auch die Antwort-Nachrichten des Funktionsblocks zu überprüfen. So enthält Bild 5 zunächst eine Transition zur Prüfung der Controller-Nachricht Allocate_StartResult, bevor die Nachricht Allocate_Result verifiziert wird, die der Funktionsblock als Antwort sendet. Bei der Verifikation einer Funktionsschnittstelle durchläuft eine MOST-Nachricht zuerst das busspezifische Verifikationsmodell, wo das korrekte Kommunikationsverhalten abgesichert wird. Ist eine Nachricht gemäß der MOST-Spezifikation korrekt, wird diese anschließend an das funktionsspezifische Verifikationsmodell weitergeleitet. Fehlverhalten ist so definiert, dass jede Busnachricht, für die im aktuellen Zustand keine Transition ausgelöst werden kann, eine Abweichung von der Spezifikation und somit einen Fehler darstellt. Deshalb enthalten die Verifikationsmodelle stets einen zusätzlichen Zustand, welcher im Fehlerfall aktiviert wird (OutOfSync-Zustand im Verifikationsmodell aus Bild 5). Dieser dedizierte Fehlerzustand protokolliert den Fehler und den Pfad im Verifikationsmodell, der zu dem Fehler geführt hat. Das Verifikationsmodell verlässt nach der fehlerhaften Nachricht wieder den dedizierten Fehlerzustand und fährt an der Stelle fort, an der die aktuelle Nachricht eine Transition auslöst. Dies ermöglicht es auch, nach einem aufgetretenen Fehler die Verifikation fortzuführen.