Project S2 develops analysis methods for the automatic verification of comprehensive correctness properties of a large-scale system (or, system of systems) such as a networked transportation system. In order to keep track of the dynamic change of the underlying communication graph, the corresponding model of a ``dynamic communication system” uses a graph to represent the state of the system. A crucial part of the analysis methods, and the principle issue in Project S2, is to analyze the dynamically changing shape of the the underlying communication graph. Our analysis methods cover this aspect of dynamic control for a maneuver of the networked transportation system (e.g., the merge of two car platoons) in addition to the game-theoretic aspect of the cooperation between the traffic participants as a prelude to the maneuver, and the timed-probabilistic aspect of the unreliable communication between the traffic participants.