Innerhalb des KORSO-Projektes verfolgt unsere Gruppe das Ziel, die Entwicklung zuverlässiger Informationssysteme auf der Basis formaler Spezifikationen zu unterst"utzen. Dazu konzentriert sich unsere Arbeit auf die Spezifikationssprache TROLL light, die es erlaubt, Teile der zu modellierenden Welt als eine Gemeinschaft nebeneinander bestehender und miteinander kommunizierender Objekte zu beschreiben. Auf diese Weise bestimmen wir sowohl die Struktur als auch das Verhalten der konzeptionellen Objekte. Unsere Spezifikationsumgebung f"ur TROLL light erlaubt die Animation von Spezifikationen ebenso wie das Beweisen von Eigenschaften der Spezifikationen unter Verwendung von Theorembeweisern.