信息物理系统的闭环模型检测

江智浩, Guangyao Chen, Yining She, Haochen Yang
Dec 27, 2020

CPS 的物理环境变化范围大，保障安全与有效性具有挑战。模型检测广泛用于 CPS 验证，但用户常因不熟悉形式化方法而构建过于具体（无法覆盖环境变化）或过于抽象（反例难以解释）的环境模型。本工作提出与环境领域无关的抽象与精化框架，在覆盖环境行为的同时提供可解释反例，使系统开发者与领域专家无需成为形式化专家也能严谨、有效地使用模型检测；并以汽车领域简单案例展示框架可行性与抽象规则的可靠性。

Abstraction
江智浩
江智浩
助理教授

江智浩是上海科技大学人机物融合系统实验室主任。

Guangyao Chen
Guangyao Chen
校友

陈光瑶已毕业，现就职于远澜私募基金。

Yining She
Yining She
博士研究生

佘一宁本科毕业于上海科技大学计算机相关专业（2018 级），现为 CMU 博士研究生。

Haochen Yang
Haochen Yang
博士研究生

杨昊辰于 2020 年获上海科技大学计算机科学硕士学位，目前于俄亥俄州立大学攻读博士学位。

相关

文章

《Computer》封面推荐论文
论文《Environment Modeling During Model Checking of Cyberphysical Systems》入选 Computer 2021 年 9 月号封面推荐。
Guangyao Chen, 江智浩
最近更新于 Sep 11, 2021
项目
《Computer》封面推荐论文

出版物

Enhancing Context Awareness with Model Checking-based Uncertainty Representation in Decision Support Systems
Model-checking-based uncertainty representation to improve context-aware decision support.
Guangyao Chen, Zeyu Li, Jicheng Gu, Yining She, Chenyang Zhu, 江智浩
引用 项目 DOI
Model checking-based decision support system for fault management: A comprehensive framework and application in electric power systems
This paper presents a model-checking-based decision-support framework for fault management in partially observable multi-agent systems. …
Guangyao Chen, Peilin He, ziqi, zixin, 江智浩
引用 项目 DOI
Environment Modeling During Model Checking of Cyber-Physical Systems
A domain-independent framework which can balance coverage and expressiveness of environment models during closed-loop model checking of Cyber-Physical Systems.
Guangyao Chen, 江智浩
引用 项目 DOI
Environment Modeling During Model Checking of Cyber-Physical Systems
Property-Driven Runtime Resolution of Feature Interactions
The feature interaction problem occurs when two or more features interact and possibly conflict with each other in unexpected ways, …
SG Raghavan, K Watanabe, E Kang, CW Lin, 江智浩, S Shiraishi
引用 项目 项目 DOI
Property-Driven Runtime Resolution of Feature Interactions
Towards Model Checking of Implantable Cardioverter Defibrillators
Ventricular Fibrillation is a disorganized electrical excitation of the heart that results in inadequate blood flow to the body. It …
H Abbas, KJ Jang, 江智浩, R Mangharam
引用 项目 项目 DOI
Towards Model Checking of Implantable Cardioverter Defibrillators
High-Confidence Medical Device Software Development
This survey examines the challenges of developing high-confidence software for implantable medical devices, especially under …
江智浩, R Mangharam
引用 项目 DOI
High-Confidence Medical Device Software Development
Safety-critical medical device development using the UPP2SF model translation tool
This paper presents UPP2SF, a model-translation tool for turning verified UPPAAL models into Simulink/Stateflow models that can be …
M Pajic, 江智浩, I Lee, O Sokolsky, R Mangharam
引用 项目 项目 DOI
Safety-critical medical device development using the UPP2SF model translation tool
Closed-loop verification of medical devices with model abstraction and refinement
This paper studies closed-loop verification of medical devices in stochastic physiological environments using a dual-chamber pacemaker …
江智浩, M Pajic, R Alur, R Mangharam
引用 项目 项目 DOI
Closed-loop verification of medical devices with model abstraction and refinement
From Verification to Implementation: A Model Translation Tool and a Pacemaker Case Study
This paper presents UPP2SF, a model-translation tool that links formally verified UPPAAL models to Simulink/Stateflow models for …
M Pajic, 江智浩, I Lee, O Sokolsky, R Mangharam
引用 项目 项目 DOI
From Verification to Implementation: A Model Translation Tool and a Pacemaker Case Study
Modeling and Verification of a Dual Chamber Implantable Pacemaker
The design and implementation of software for medical devices is challenging due to their rapidly increasing functionality and the …
江智浩, M Pajic, S Moarref, R Alur, R Mangharam
引用 项目 项目 DOI
Modeling and Verification of a Dual Chamber Implantable Pacemaker
Cyber Physical Modeling of Implantable Cardiac Medical Devices
The design of bug-free and safe medical device software is challenging, especially in complex implantable devices that control and …
江智浩, M Pajic, R Mangharam
引用 项目 项目 DOI
Cyber Physical Modeling of Implantable Cardiac Medical Devices