Generierung von kurzen Testsequenzen für LOTOS-Verhaltensspezifikationen mit Hilfe von Fehlermodellen.