Statistical Model Checking of Systems of Systems: An Industrial Approach
Verification statistique de systèmes de systèmes : une approche industrielle
Résumé
Ensuring a correct behaviour of Systems of Systems (SoS) has a significant social impact. Their complexity and inherent dynamicity pose a serious challenge to traditional design methodologies. We propose a methodology and a tool-chain supporting continuous validation
of SoS behaviour against formal requirements, based on a scalable formal verification technique known as Statistical Model Checking (SMC). We integrate SMC with existing industrial practice, by addressing both methodological and technological issues. Our contribution is summarized as follows: (1) a methodology for continuous and scalable validation of SoS formal requirements; (2) a natural-language based formal specification language able to express complex SoS requirements; (3) adoption of widely used industry standards for simulation and heterogeneous systems integration (FMI and UPDM); (4) development of a robust SMC tool-chain integrated with system design tools used in practice. We illustrate the application of our SMC tool-chain and the obtained results on an industrial case study from the DANSE project.
S'assurer qu'un Système de Systèmes (SdS) se comporte correctement est essentiel pour notre société. La complexité et le côté dynamique inhérent à ce type de systèmes constitue un défi pour les méthodes de conception traditionnelles. Nous proposons une méthodologie et une chaîne d'outils permettant de valider la conformité du comportement d'un SdS vis-à-vis d'un ensemble de propriétés formelles. Cette méthodologie est fondée sur la vérification statistique de modèles (SMC). Nous intégrons SMC dans les pratiques industrielles existantes, en résolvant des problèmes méthodologiques et technologiques. Notre contribution comporte: (1) une méthodologie passant à l'échelle pour valider la conformité d'un SdS avec des propriétés formelles ; (2) un langage proche du langage naturel pour exprimer les propriétés formelles complexes attendues du SdS ; (3) l'adoption de standards pour la simulation et l'intégration de modèles hétérogènes largement utilisés dans l'industrie (FMI et UPDM); (4) le développement d'une chaîne d'outils robuste intégrant les outils de conception de systèmes utilisés par les praticiens. Nous illustrons l'utilisation de notre chaîne d'outils et les résultat obtenus avec un cas d'étude industriel provenant du projet DANSE.
Origine : Fichiers produits par l'(les) auteur(s)