Skip to Main content Skip to Navigation
Other publications

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.
Complete list of metadata

Cited literature [10 references]  Display  Hide  Download

https://hal.inria.fr/hal-01090330
Contributor : Jean Quilbeuf <>
Submitted on : Wednesday, December 3, 2014 - 1:27:06 PM
Last modification on : Thursday, January 7, 2021 - 4:22:45 PM
Long-term archiving on: : Saturday, April 15, 2017 - 2:42:58 AM

File

sos_contract_verification.pdf
Files produced by the author(s)

Identifiers

Citation

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⟩

Share

Metrics

Record views

1098

Files downloads

399