Das Projekt S2 entwickelt Analysemethoden für die automatische Verifikation von ganzheitlichen Korrektheitseigenschaften eines Großsystems (oder, eines Systems von Systemen) wie z.B. ein vernetztes Transportsystem. Um den dynamischen Wechsel des unterliegenden Kommunikationsgraphen zu berücksichtigen, benutzt das zugehörige Modell des „Dynamischen Kommunikationssystems” einen Graphen zur Zustandsrepräsentation. Ein wichtiger Bestandteil der Analysemethoden, und das Hauptproblem im Projekt S2, ist es, die sich dynamisch ändernde Form („Shape“) des unterliegenden Kommunikationsgraphen zu analysieren. Unsere Analysemethoden decken nicht nur diesen Aspekt der dynamischen Kontrolle für ein Manöver eines Vernetzten Transportsystems (z.B. das Verschmelzen zweir Auto-Gruppen) ab, sondern zusätzlich den spieltheoretischen Aspekt der Kooperation zwischen den Verkehrsteilnehmern zur Einleitung des Manövers, und den zeitlich-probabilistischen Aspekt der unzuverlässigen Kommunikation zwischen den Verkehrsteilnehmern.