An Application of SMC to continuous validation of heterogeneous systems
Journal Title: EAI Endorsed Transactions on Industrial Networks and Intelligent Systems - Year 2017, Vol 4, Issue 10
Abstract
This paper considers the rigorous design of Systems of Systems (SoS), i.e. systems composed of a set of heterogeneous components whose number evolves with time. Such components cooperate to accomplish functions that they could not achieve in isolation. Examples of SoS include smart cities or airport management system. The dynamical evolution of SoS behavior and architecture makes it impossible to design an appropriate solution beforehand. Consequently, existing approaches build on an iterative process that takes SoS evolution into account. A key challenge in this process is the ability to reason about and analyze a given view of the SoS (on a fixed number of SoS constituents) with respect to a set of goals, and use the results to eventually predict the evolution of the SoS. To address this challenge, we rely 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: (1) a methodology for validation of SoS formal requirements; (2) a formal specification language able to express complex SoS requirements; (3) the adoption of current industry standards for simulation and heterogeneous systems integration ; (4) a robust SMC tool-chain 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.
Authors and Affiliations
Alexandre Arnold, Massimo Baleani, Alberto Ferrari, Marco Marazza, Valerio Senni, Axel Legay, Jean Quilbeuf, Christoph Etzien
Keywords
Related Articles
- EP ID EP46059
- DOI http://dx.doi.org/10.4108/eai.1-2-2017.152154
- Views 298
- Downloads 0
Eigenvalue-based Detection Techniques Using Finite Dimensional Complex Random Matrix Theory: A Review
Detection of primary users without requiring information of signal is of great importance in spectrum sensing (SS) in Cognitive Radio. Therefore, in recent years, eigenvalue based spectrum sensing algorithms are under th...
Cooperative Spectrum-Sharing with Two-Way AF Relaying in the Presence of Direct Communications
In this paper, we investigate a three-phase two-way (TW) amplify-and-forward (AF) relaying for cognitive radio networks. By utilizing the direct communications, the end user can employ diversity combining techniques, i.e...
Empirical analysis of IPv6 transition technologies using the IPv6 Network Evaluation Testbed
IPv6 has yet to become more than a worthy successor of IPv4, which remains, for now, the dominant Internet Protocol. This is due to the complicated transition period through which the Internet will have to go, until IPv6...
TiPeNeSS: A Timed Petri Net Simulator Software with Generally Distributed Firing Delays
Performance analysis can be carried out in several ways, especially in case of Markovian models. In order to interpret high level of abstraction, we often use modeling tools like timed Petri nets (TPNs). Although some su...
Gatewaying theWireless Sensor Networks
With the dev elopmen t of Internet of Things (IoT), bridging wireless sensor netw orks (WSNs) with other netw orks has become importan t. We divide bridging solutions into tw o categ ories: the hardw are solutions and th...