In Scala werden eingebettete domänenspezifische Sprache häufig für die Beschreibung von Nebenläufigkeitsproblemen verwendet. Bestehende Byte-Code-basierte Model-Checkern überprüfen auch das Laufzeitsystem einer solchen Sprache, was diesen Prozess komplexer macht als in der Praxis notwendig.

In dieser Arbeit wurden drei unterschiedliche explicit state Model-Checker entwickelt und deren Eigenschaften untersucht. Diese Model-Checker beschreiben ausschließlich nur das Verhalten der jeweiligen Sprache.