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 323
- Downloads 0
Natural Disaster and Environmental Monitoring System for Smart Cities: Design and Installation Insights
Climate change is mainly caused by human activities. Consequently, natural disasters such as flooding, storm, and drought are attacking people at high frequency and extreme damage. Besides, many megacities have been facin...
Outage Probability of Vehicular Networks under Unreliable Backhaul
This paper presents for the first time a heterogeneous vehicular model with multiple moving small cells and a moving receiver with unreliable backhaul. In this system, a macro-base station connects to multiple moving smal...
Scalable SOCP-based localization technique for wireless sensor network
Node localization is one of the essential requirements to most applications of wireless sensor networks. This paper presents a detailed implementation of a centralized localization technique for WSNs based on Second Orde...
Ant Colony Optimization Based Model Checking Extended by Smell-like Pheromone
Model Checking is a technique for automatically checking the model representing software or hardware about whether they satisfy the corresponding specifications. Traditionally, the model checking uses deterministic algor...
An Investigation of Performance Analysis of Anomaly Detection Techniques for Big Data in SCADA Systems
Anomaly detection is an important aspect of data mining, where the main objective is to identify anomalous or unusual data from a given dataset. However, there is no formal categorization of application-specific anomaly...