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 317
- Downloads 0
VIRTUAL TABLE-SIMULATOR FOR MONITORING DISTRIBUTED OBJECTS
There is presented a determination to the concept of "a distributed subobject for monitoring". There are revealed the common features of such objects. There are analyzed the virtual and hardware cloud computing technolog...
A2Ba: Adaptive Background Modelling for Visual Aerial Surveillance Conditions
Background modelling algorithms are widely used to define a part of an image that most time remains stationary in a video. In surveillance tasks, this model helps to recognize those outlier objects in an area under monit...
Exact Outage Analysis of Cognitive Energy Harvesting Relaying Networks under Physical Layer Security
In this paper, we study the secure communication of cognitive energy harvesting relay networks when there exist multiple eaves droppers who can overhear the message of the second hop, and multiple primary users are prese...
Information seeking behaviour and purchasing decision: case study in digital cameras
This case study explores the information seeking behaviour of digital camera consumers based on Assael’s consumer information acquisition and processing model. 135 responses were received from potential target group who...
Fundamental Approach for Analysis of Dynamic Characteristics of Fixtures
Present work is aimed at research of locating and clamping process of prismatic parts in fixtures during the machining on drilling-milling-boring machines. The fundamental approach for developing mathematical modeling of...