An Application of SMC to continuous validation of heterogeneous systems

Alexandre Arnold 1 Massimo Baleani 2 Alberto Ferrari 2 Marco Marazza 2 Valerio Senni 2 Axel Legay 3 Jean Quilbeuf 4, 3 Christoph Etzien 5
1 EADS - European Aeronautic Defense and Space
2 ALES - Advanced Laboratories on Embedded Systems [Roma]
3 TAMIS - Threat Analysis and Mitigation for Information Security
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
4 ArchWare
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires
5 OFFIS - Institute for Information Technology [Oldenburg]
Abstract : This paper considers the rigorous design of Systems of Systems (SoS), i.e. systems composed of a series of heterogeneous components whose number evolves with time. Such components coalize to accomplish functions that they could not achieve alone. Examples of SoS includes (among many others) almost any application of the Internet of things such as smart cities or airport management system. Dynamical evolution of SoS makes it impossible to design an appropriate solution beforehand. Consequently, existing approaches build on an iterative process that takes its evolution into account. A key challenge in this process is the ability to reason and analyze a given view of the SoS, i.e. verifying a series of goals on a fixed number of SoS constituents, and use the results to eventually predict its evolution. To address this challenge, we propose a methodology and a tool-chain supporting continuous validation of SoS behavior against formal requirements, based on a scalable formal verification technique known as Statistical Model Checking (SMC). SMC quantifies how close the current view is from achieving a given mission. 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 toolchain integrated with system design tools used in practice. We illustrate the application of our SMC tool-chain and the obtained results on a case study.
Keywords : statistical model checking Systems of systems tool- chain FMI simulation.
Type de document :
Communication dans un congrès
Simutools 2016 - Ninth EAI International Conference on Simulation Tools and Techniques, Aug 2016, Prague, Czech Republic. Proceedings of the Ninth EAI International Conference on Simulation Tools and Techniques
Liste complète des métadonnées

Littérature citée [37 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/hal-01390487
Contributeur : Jean Quilbeuf <>
Soumis le : lundi 7 novembre 2016 - 12:54:00
Dernière modification le : mercredi 16 mai 2018 - 11:24:11
Document(s) archivé(s) le : mercredi 8 février 2017 - 14:10:04

Fichier

SIMUTOOLS.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01390487, version 1

Collections

INRIA | IRISA_UBS | IRISA | CENTRALESUPELEC | UBS | UR1-UFR-ISTIC | UNIV-RENNES

Citation

Alexandre Arnold, Massimo Baleani, Alberto Ferrari, Marco Marazza, Valerio Senni, et al.. An Application of SMC to continuous validation of heterogeneous systems. Simutools 2016 - Ninth EAI International Conference on Simulation Tools and Techniques, Aug 2016, Prague, Czech Republic. Proceedings of the Ninth EAI International Conference on Simulation Tools and Techniques. 〈hal-01390487〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

728

Téléchargements de fichiers

135

Contact


archive-ouverte@inria.fr