Please use this identifier to cite or link to this item: http://elea.unisa.it:8080/xmlui/handle/10556/4246
Title: Model Checking Cyber-Physical Systems
Authors: Driouich, Youssef
Chiacchio, Pasquale
Parente, Domenico
Keywords: Cyber-physical systems
Formal-methods
Automatic verification
Issue Date: 12-Mar-2019
Publisher: Universita degli studi di Salerno
Abstract: Cyber-Physical Systems (CPSs) are integrations of computation with physical processes. Applications of CPS arguably have the potential to overshadow the 20-th century IT revolution. Nowadays, CPSs application to many sectors like Smart Grids, Transportation, and Health help us run our lives and businesses smoothly, successfully and safely. Since malfunctions in these CPSs can have serious, expensive, sometimes fatal consequences, Simulation-based Veri cation (SBV) tools are vital to minimize the probability of errors occurring during the development process and beyond. Their applicability is supported by the increasingly widespread use of Model Based Design (MBD) tools. MBD enables the simulation of CPS models in order to check for their correct behaviour from the very initial design phase. The disadvantage is that SBV for complex CPSs is an extremely resources and time-consuming process, which typically requires several months of simulation. Current SBV tools are aimed at accelerating the veri cation process with mul- tiple simulators working simultaneously. To this end, they compute all the scenarios in advance in such a way as to split and simulate them in parallel. Nevertheless, there are still limitations that prevent a more widespread adop- tion of SBV tools. To this end, we present a MBD methodology aiming the acausual modeling and veri cation via formal-methods, speci cally the model checking techniques, the system under veri cation (SUV). Our approach relies basically on: Firstly, the analysis of the steady-states of the CPS and the bound- ing technique of the system's state in parallel with the simulation in order to identify the state space of the system simulating it only once, then represent it as a Finite State Machine (FSM). Secondly, exhaustively verify the resulted FSM using a symbolic model checker and express the desired properties in classical temporal logic. The application to a power management system is presented as a case study. [edited by Author]
Description: 2017 - 2018
URI: http://elea.unisa.it:8080/xmlui/handle/10556/4246
http://dx.doi.org/10.14273/unisa-2452
Appears in Collections:Informatica ed Ingegneria dell'Informazione

Files in This Item:
File Description SizeFormat 
tesi di dottorato Y. Driouich.pdftesi di dottorato3,08 MBAdobe PDFView/Open
abstract in inglese Y. Driouich.pdfabstract in inglese a cura dell'Autore40,94 kBAdobe PDFView/Open
abstract in italiano Y. Driouich.pdfabstract in italiano a cura dell'Autore40,29 kBAdobe PDFView/Open


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.