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 11
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 Beleani, Alberto Ferrari, Marco Marazza, Valerio Senni, Axel Legay, Jean Quilbeuf, Christoph Etzien
Keywords
Related Articles
- EP ID EP46065
- DOI http://dx.doi.org/10.4108/eai.21-12-2017.153500
- Views 286
- Downloads 0
Comparative Study on Power Gating Techniques for Lower Power Delay Product, Smaller Power Loss, Faster Wakeup Time
The power gating is one of the most popular reduction leakage techniques. We make comparison among various power gating schemes in terms of power delay product, energy loss, and wake-up time using the 45-nm Predictive Te...
A Review of Research on Acoustic Detection of Heat Exchanger Tube
Leakage in heat exchanger tubes can result in unreliable products and dangerous situations, which could cause great economic losses. Along with fast development of modern acoustic detection technology, using acoustic sig...
Security-Reliability Analysis of Multi-hop LEACH Protocol with Fountain Codes and Cooperative Jamming
In this paper, we investigate trade-off between security and reliability of Fountain codes (FCs) based low-energy adaptive clustering hierarchy (LEACH) networks, where the encoded packets are sent to the destination by u...
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...
Improving ns-3 Emulation Support in Real-World Networking Scenarios
A common problem in networking research and development is the duplicate effort of writing simulation and implementation code. This duplication can be avoided through the use of fast-prototyping methodologies, which enab...