SoS contract verification using statistical model checking - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Autre Publication Année : 2013

SoS contract verification using statistical model checking

Résumé

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.
Fichier principal
Vignette du fichier
sos_contract_verification.pdf (1.46 Mo) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01090330 , version 1 (03-12-2014)

Identifiants

Citer

Alessandro Mignogna, Leonardo Mangeruca, Benoît Boyer, Axel Legay, Alexandre Arnold. SoS contract verification using statistical model checking. 2013, pp.67 - 83. ⟨10.4204/EPTCS.133.7⟩. ⟨hal-01090330⟩
688 Consultations
204 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More