Contracts and Behavioral Patterns for SoS: The EU IP DANSE approach
This work addresses the problem of formal verification for SoS in defense and aerospace domains, but it appears incremental as it builds on existing tools and methods.
The paper tackles the challenge of specifying and analyzing System of Systems (SoS) requirements by introducing a tool chain that uses high-level modeling with UPDM and behavioral pattern contracts, combined with low-level simulation and statistical model checking, applied to a case study at EADS Innovation Works.
This paper presents some of the results of the first year of DANSE, one of the first EU IP projects dedicated to SoS. Concretely, we offer a tool chain that allows to specify SoS and SoS requirements at high level, and analyse them using powerful toolsets coming from the formal verification area. At the high level, we use UPDM, the system model provided by the british army as well as a new type of contract based on behavioral patterns. At low level, we rely on a powerful simulation toolset combined with recent advances from the area of statistical model checking. The approach has been applied to a case study developed at EADS Innovation Works.