返回
A framework for modeling and analyzing cyber-physical systems using statistical model checking
DOI:10.1016/j.iot.2023.100732.png)
摘要
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.
Keyword:
System Modeling Language
Enhanced Activity Calculus
Cyber-Physical systems
Model transformation
model-based verification
Safety-critical
Statistical model checking
Priced timed automata
期刊
IF:
7.6
论文数:
1.9K
被引数:
6.9K
机构
引用论文
Early identification of the critical view of safety in laparoscopic cholecystectomy using indocyanine green fluorescence cholangiography: A randomised controlled study使用吲哚菁绿荧光胆管造影术早期识别腹腔镜胆囊切除术安全性的关键观点: 一项随机对照研究
Tracking a system of shared autonomous vehicles across the Austin, Texas network using agent-based simulation
TRANSPORTATION
IF3.3

