Monte Carlo Based Statistical Model Checking of Cyber-Physical Systems: A Review
The ever-increasing deployment of autonomous Cyber-Physical Systems (CPSs) (e.g., autonomous cars, UAV) exacerbates the need for efficient formal verification methods. In this setting, the main obstacle to overcome is the huge number of scenarios to be evaluated. Statistical Model Checking (SMC) is...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
MDPI AG
2020-12-01
|
| Series: | Information |
| Subjects: | |
| Online Access: | https://www.mdpi.com/2078-2489/11/12/588 |
| _version_ | 1797543999175655424 |
|---|---|
| author | Angela Pappagallo Annalisa Massini Enrico Tronci |
| author_facet | Angela Pappagallo Annalisa Massini Enrico Tronci |
| author_sort | Angela Pappagallo |
| collection | DOAJ |
| description | The ever-increasing deployment of autonomous Cyber-Physical Systems (CPSs) (e.g., autonomous cars, UAV) exacerbates the need for efficient formal verification methods. In this setting, the main obstacle to overcome is the huge number of scenarios to be evaluated. Statistical Model Checking (SMC) is a simulation-based approach that holds the promise to overcome such an obstacle by using statistical methods in order to sample the set of scenarios. Many SMC tools exist, and they have been reviewed in several works. In this paper, we will overview Monte Carlo-based SMC tools in order to provide selection criteria based on Key Performance Indicators (KPIs) for the verification activity (e.g., minimize verification time or cost) as well as on the environment features, the kind of system model, the language used to define the requirements to be verified, the statistical inference approach used, and the algorithm implementing it. Furthermore, we will identify open research challenges in the field of (SMC) tools. |
| first_indexed | 2024-03-10T13:53:25Z |
| format | Article |
| id | doaj.art-58155849d89d4be28ef57d78a6c66e72 |
| institution | Directory Open Access Journal |
| issn | 2078-2489 |
| language | English |
| last_indexed | 2024-03-10T13:53:25Z |
| publishDate | 2020-12-01 |
| publisher | MDPI AG |
| record_format | Article |
| series | Information |
| spelling | doaj.art-58155849d89d4be28ef57d78a6c66e722023-11-21T01:51:14ZengMDPI AGInformation2078-24892020-12-01111258810.3390/info11120588Monte Carlo Based Statistical Model Checking of Cyber-Physical Systems: A ReviewAngela Pappagallo0Annalisa Massini1Enrico Tronci2Computer Science Department, Sapienza University of Rome, Via Salaria 113, 00198 Rome, ItalyComputer Science Department, Sapienza University of Rome, Via Salaria 113, 00198 Rome, ItalyComputer Science Department, Sapienza University of Rome, Via Salaria 113, 00198 Rome, ItalyThe ever-increasing deployment of autonomous Cyber-Physical Systems (CPSs) (e.g., autonomous cars, UAV) exacerbates the need for efficient formal verification methods. In this setting, the main obstacle to overcome is the huge number of scenarios to be evaluated. Statistical Model Checking (SMC) is a simulation-based approach that holds the promise to overcome such an obstacle by using statistical methods in order to sample the set of scenarios. Many SMC tools exist, and they have been reviewed in several works. In this paper, we will overview Monte Carlo-based SMC tools in order to provide selection criteria based on Key Performance Indicators (KPIs) for the verification activity (e.g., minimize verification time or cost) as well as on the environment features, the kind of system model, the language used to define the requirements to be verified, the statistical inference approach used, and the algorithm implementing it. Furthermore, we will identify open research challenges in the field of (SMC) tools.https://www.mdpi.com/2078-2489/11/12/588statistical model checkingCyber-Physical SystemsMonte Carlo sampling |
| spellingShingle | Angela Pappagallo Annalisa Massini Enrico Tronci Monte Carlo Based Statistical Model Checking of Cyber-Physical Systems: A Review Information statistical model checking Cyber-Physical Systems Monte Carlo sampling |
| title | Monte Carlo Based Statistical Model Checking of Cyber-Physical Systems: A Review |
| title_full | Monte Carlo Based Statistical Model Checking of Cyber-Physical Systems: A Review |
| title_fullStr | Monte Carlo Based Statistical Model Checking of Cyber-Physical Systems: A Review |
| title_full_unstemmed | Monte Carlo Based Statistical Model Checking of Cyber-Physical Systems: A Review |
| title_short | Monte Carlo Based Statistical Model Checking of Cyber-Physical Systems: A Review |
| title_sort | monte carlo based statistical model checking of cyber physical systems a review |
| topic | statistical model checking Cyber-Physical Systems Monte Carlo sampling |
| url | https://www.mdpi.com/2078-2489/11/12/588 |
| work_keys_str_mv | AT angelapappagallo montecarlobasedstatisticalmodelcheckingofcyberphysicalsystemsareview AT annalisamassini montecarlobasedstatisticalmodelcheckingofcyberphysicalsystemsareview AT enricotronci montecarlobasedstatisticalmodelcheckingofcyberphysicalsystemsareview |