Show simple item record

dc.contributor.authorDriouich, Youssef
dc.date.accessioned2020-03-17T09:48:57Z
dc.date.available2020-03-17T09:48:57Z
dc.date.issued2019-03-12
dc.identifier.urihttp://elea.unisa.it:8080/xmlui/handle/10556/4246
dc.identifier.urihttp://dx.doi.org/10.14273/unisa-2452
dc.description2017 - 2018it_IT
dc.description.abstractCyber-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]it_IT
dc.language.isoenit_IT
dc.publisherUniversita degli studi di Salernoit_IT
dc.subjectCyber-physical systemsit_IT
dc.subjectFormal-methodsit_IT
dc.subjectAutomatic verificationit_IT
dc.titleModel Checking Cyber-Physical Systemsit_IT
dc.typeDoctoral Thesisit_IT
dc.subject.miurINF/01 INFORMATICAit_IT
dc.contributor.coordinatoreChiacchio, Pasqualeit_IT
dc.description.cicloXXX cicloit_IT
dc.contributor.tutorParente, Domenicoit_IT
dc.identifier.DipartimentoIngegneria dell’Informazione ed Elettrica e Matematica Applicatait_IT
 Find Full text

Files in this item

Thumbnail
Thumbnail
Thumbnail

This item appears in the following Collection(s)

Show simple item record