A framework for modeling and analyzing cyber-physical systems using statistical model checking

Abdel-Latif Alshalalfah

doi:10.1016/j.iot.2023.100732

Return

A framework for modeling and analyzing cyber-physical systems using statistical model checking

2023-07-01

PRE

Abdel-Latif Alshalalfah *

Otmane Aı̈t Mohamed

Samir Ouchani

DOI：10.1016/j.iot.2023.100732

Original

Original request for help

Save

Abstract

En 中文

The trustworthiness of a cyber-physical system is essential for it to be qualified for utilization in most real-life deployments. This is especially critical for systems that deal with precious human lives. Although these safety-critical systems can be investigated using both experimental testing and model-based verification, accurate models have the potential to permit risk-free mimicking of the system behavior even in the most extreme scenarios. To overcome the CPS modeling and design challenges, the INCOSE/OMG standard System Modeling Language (SysML) is utilized in this work to accurately specify cyber-physical systems. For that, a bounded set of SysML constructs are defined to precisely capture the semantics of continuous-time and discrete-time system behaviors. Then, the SysML constructs are substituted by developing a new algebra, called Enhanced Activity Calculus (EAC). So, EAC helps construct equivalent priced timed automata models by developing a new systematic procedure to correctly translate the SysML models into the statistical model checking tool UPPAAL-SMC inputs. The latter checks whether the system is correct and safe or not. Moreover, the soundness of the developed translation mechanism has been proved and its effectiveness has been shown on a real use case, namely the artificial pancreas.

Keywords:

System Modeling Language

Enhanced Activity Calculus

Cyber-Physical systems

Model transformation

model-based verification

Safety-critical

Statistical model checking

Priced timed automata