| Autor: |
Alessandro Mignogna, Leonardo Mangeruca, Benoît Boyer, Axel Legay, Alexandre Arnold |
| Jazyk: |
angličtina |
| Rok vydání: |
2013 |
| Předmět: |
|
| Zdroj: |
Electronic Proceedings in Theoretical Computer Science, Vol 133, Iss Proc. AiSoS 2013, Pp 67-83 (2013) |
| Druh dokumentu: |
article |
| ISSN: |
2075-2180 |
| DOI: |
10.4204/EPTCS.133.7 |
| Popis: |
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. |
| Databáze: |
Directory of Open Access Journals |
| Externí odkaz: |
|
