Project Group S focuses on techniques to support the global analysis of the interplay between different systems, or between subsystems, thus addressing both inter-system and system-level design. Typical instances in the train system domain relate to the interaction between trains and track-side elements such as RBC, s, or between the different components of the on-board electronic subsystems of a train. The overall challenge for Project Group S is thus the need to address complete systems, or even systems of systems, demanding dedicated techniques to cater for the sheer complexity of resulting models. Project S1 addresses this by automating compositional verification; it uses learning strategies and combinations of abstraction techniques, game theory, and SAT and model checking based verification methods to automatically synthesize assumptions, allowing to reduce global verification of (potentially only partially specified) system level designs to local verification tasks. The particular challenges of inter-system coordination protocols, which typically require dynamically changing communication structures and must address systems entering and leaving surveillance regions, are attacked in S2 with a combination of static analysis techniques, abstraction techniques, and symmetry arguments to reduce the verification of such coordination protocols to finite state verification problems. Project S3 provides formal proofs of system dependability requirements through stochastic model checking of system models, taking into account failure models and component failure behaviors, while deriving safety requirements for subsequent design steps.

By addressing complete systems and their interplay, Project Group S provides methods for reducing global verification tasks to smaller problem instances (S1, S2) and dependability analysis, which inherently requires global system analysis. Projects S1 and S2 complement each other, in that verification instances resulting from the reduction methods of S2 can be further decomposed using techniques of S1. Models used will reflect the particular complexity dimension attacked in each project, providing sufficiently rich structuring methods to asynchronously compose transition systems, supporting their dynamic creation and destruction and dynamic communication structures for S2, and using extended Markov Processes in S3. Later project phases will enrich the class of models, allowing to deal with real-time and hybrid component models, and extend decomposition theorems to such richer classes of models, thus paving the way for realizing the AVACS vision, where an overall verification methodology invokes such decomposition theorems, unfolding a proof tree for global problems to a level where verification tasks can be discharged with the verification methods developed in Project Groups R and H.