SoS contract verification using statistical model checking

Abstract : Exhaustive formal verification for systems of systems (SoS) is impractical and cannot be applied on a large scale. In this paper we propose to use statistical model checking for efficient verification of SoS. We address three relevant aspects for systems of systems: 1) the model of the SoS, which includes stochastic aspects; 2) the formalization of the SoS requirements in the form of contracts; 3) the tool-chain to support statistical model checking for SoS. We adapt the SMC technique for application to heterogeneous SoS. We extend the UPDM/SysML specification language to express the SoS requirements that the implemented strategies over the SoS must satisfy. The requirements are specified with a new contract language specifically designed for SoS, targeting a high-level English-pattern language, but relying on an accurate semantics given by the standard temporal logics. The contracts are verified against the UPDM/SysML specification using the Statistical Model Checker (SMC) PLASMA combined with the simulation engine DESYRE, which integrates heterogeneous behavioral models through the functional mock-up interface (FMI) standard. The tool-chain allows computing an estimation of the satisfiability of the contracts by the SoS. The results help the system architect to trade-off different solutions to guide the evolution of the SoS.
Type de document :
Autre publication
Workshop paper presenting the Toolchain to be produced by the DANSE project for modelling and ver.. 2013, pp.67 - 83. 〈10.4204/EPTCS.133.7〉
Liste complète des métadonnées

Littérature citée [10 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01090330
Contributeur : Jean Quilbeuf <>
Soumis le : mercredi 3 décembre 2014 - 13:27:06
Dernière modification le : mercredi 11 avril 2018 - 02:00:27
Document(s) archivé(s) le : samedi 15 avril 2017 - 02:42:58

Fichier

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

Identifiants

Citation

Alessandro Mignogna, Leonardo Mangeruca, Benoît Boyer, Axel Legay, Alexandre Arnold. SoS contract verification using statistical model checking. Workshop paper presenting the Toolchain to be produced by the DANSE project for modelling and ver.. 2013, pp.67 - 83. 〈10.4204/EPTCS.133.7〉. 〈hal-01090330〉

Partager

Métriques

Consultations de la notice

482

Téléchargements de fichiers

131