arrow
返回

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

delete2023-07-01
delete3
PRE
AI
A
Abdel-Latif Alshalalfah *
O
Otmane Aı̈t Mohamed
S
Samir Ouchani
DOI:10.1016/j.iot.2023.100732delete
delete原文链接
delete原文求助
delete分享
delete收藏
摘要

摘要

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

期刊

Internet of Things 封面图
Internet of Things
IF:
7.6
论文数:
1.9K
被引数:
6.9K

机构

C
concordia university - canada
学者数:
8.0K
论文数: 8.9K
被引数: 4
引用论文

引用论文

Model-Driven Safety Analysis of Closed-Loop Medical Systems
err2014-02-01
err75
errOAAI
errPajic, Miroslav; Mangharam, Rahul; Sokolsky, Oleg; Arney, David; Goldman, Julian; Lee, Insup
err分享
err收藏
Tracking a system of shared autonomous vehicles across the Austin, Texas network using agent-based simulation
err2017-08-23
err181
errOAAI
errLiu, Jun; Kockelman, Kara M.; Boesch, Patrick M.; Ciari, Francesco
err分享
err收藏
Prevención y tratamiento de la enfermedad infecciosa en personas con diabetes
err2019-03-01
err0
PREAI
errF. López-Simarro; E. Redondo Margüello; J.J. Mediavilla Bravo; T. Soriano Llora; J. Iturralde Iriso; A. Hormigo Pozo
err分享
err收藏
An evaluation framework for energy aware buildings using statistical model checking
err2012-12-29
err33
PREAI
errDavid, Alexandre; Du DeHui; Larsen, Kim G.; Mikucionis, Marius; Skou, Arne
err分享
err收藏
学者 查看更多内容