Home > Research > Publications & Outputs > Practical Formal Verification for Model Based D...

Research

Associated organisational units

Links

Text available via DOI:

Keywords

View graph of relations

Practical Formal Verification for Model Based Development of Cyber-Physical Systems

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Conference contribution/Paper › peer-review

Published

Standard

Practical Formal Verification for Model Based Development of Cyber-Physical Systems. / Ishigooka, T.; Saissi, H.; Piper, T. et al.
2016 IEEE Intl Conference on Computational Science and Engineering (CSE) and IEEE Intl Conference on Embedded and Ubiquitous Computing (EUC) and 15th Intl Symposium on Distributed Computing and Applications for Business Engineering (DCABES). IEEE, 2016. p. 1-8.

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Conference contribution/Paper › peer-review

Harvard

Ishigooka, T, Saissi, H, Piper, T, Winter, S & Suri, N 2016, Practical Formal Verification for Model Based Development of Cyber-Physical Systems. in 2016 IEEE Intl Conference on Computational Science and Engineering (CSE) and IEEE Intl Conference on Embedded and Ubiquitous Computing (EUC) and 15th Intl Symposium on Distributed Computing and Applications for Business Engineering (DCABES). IEEE, pp. 1-8. https://doi.org/10.1109/CSE-EUC-DCABES.2016.154

APA

Ishigooka, T., Saissi, H., Piper, T., Winter, S., & Suri, N. (2016). Practical Formal Verification for Model Based Development of Cyber-Physical Systems. In 2016 IEEE Intl Conference on Computational Science and Engineering (CSE) and IEEE Intl Conference on Embedded and Ubiquitous Computing (EUC) and 15th Intl Symposium on Distributed Computing and Applications for Business Engineering (DCABES) (pp. 1-8). IEEE. https://doi.org/10.1109/CSE-EUC-DCABES.2016.154

Vancouver

Ishigooka T, Saissi H, Piper T, Winter S, Suri N. Practical Formal Verification for Model Based Development of Cyber-Physical Systems. In 2016 IEEE Intl Conference on Computational Science and Engineering (CSE) and IEEE Intl Conference on Embedded and Ubiquitous Computing (EUC) and 15th Intl Symposium on Distributed Computing and Applications for Business Engineering (DCABES). IEEE. 2016. p. 1-8 doi: 10.1109/CSE-EUC-DCABES.2016.154

Author

Ishigooka, T. ; Saissi, H. ; Piper, T. et al. / Practical Formal Verification for Model Based Development of Cyber-Physical Systems. 2016 IEEE Intl Conference on Computational Science and Engineering (CSE) and IEEE Intl Conference on Embedded and Ubiquitous Computing (EUC) and 15th Intl Symposium on Distributed Computing and Applications for Business Engineering (DCABES). IEEE, 2016. pp. 1-8

Bibtex

@inproceedings{bcbaf9d4034c444caa709a57c9791676,
title = "Practical Formal Verification for Model Based Development of Cyber-Physical Systems",
abstract = "The application of cyber-physical systems (CPSs) in safety-critical applications requires rigorous verification of their functional correctness and safety-relevant properties. We propose a practical verification framework which enables to fill the gaps between model-based development and the formal verification process seamlessly connecting them. The verification framework consists of (a) a model transformation method, which automatically transforms the plant models of CPSs including differential algebraic equations (DAE) to equivalent models without DAE to reduce verification complexity induced by DAE solver execution, and (b) a model simplification method, which automatically simplifies bond-graph models by replacing complex bond-graph components with simpler components for further verification overhead reductions. We successfully applied the proposed verification framework for safety verification of an automotive brake control system. The results of the study demonstrate that the automated model transformations of the CPS models yield significant verification complexity reductions without impairing the ability to detect unsafe behavior of the brake control system in a formal verification based on symbolic execution. {\textcopyright} 2016 IEEE.",
keywords = "bond-graph model, cyber-physical systems, Formal verification, model transformation, model-based development, signal-flow model, Algebra, Automobile parts and equipment, Brakes, Control systems, Cyber Physical System, Differential equations, Distributed computer systems, Embedded systems, Flow graphs, Graph theory, Reduction, Safety engineering, Signal flow graphs, Ubiquitous computing, Automated model transformations, Bond graph model, Cyber physical systems (CPSs), Differential algebraic equations, Model based development, Model transformation, Model transformation methods, Signal flow",
author = "T. Ishigooka and H. Saissi and T. Piper and S. Winter and Neeraj Suri",
year = "2016",
month = aug,
day = "24",
doi = "10.1109/CSE-EUC-DCABES.2016.154",
language = "English",
pages = "1--8",
booktitle = "2016 IEEE Intl Conference on Computational Science and Engineering (CSE) and IEEE Intl Conference on Embedded and Ubiquitous Computing (EUC) and 15th Intl Symposium on Distributed Computing and Applications for Business Engineering (DCABES)",
publisher = "IEEE",

}

RIS

TY - GEN

T1 - Practical Formal Verification for Model Based Development of Cyber-Physical Systems

AU - Ishigooka, T.

AU - Saissi, H.

AU - Piper, T.

AU - Winter, S.

AU - Suri, Neeraj

PY - 2016/8/24

Y1 - 2016/8/24

N2 - The application of cyber-physical systems (CPSs) in safety-critical applications requires rigorous verification of their functional correctness and safety-relevant properties. We propose a practical verification framework which enables to fill the gaps between model-based development and the formal verification process seamlessly connecting them. The verification framework consists of (a) a model transformation method, which automatically transforms the plant models of CPSs including differential algebraic equations (DAE) to equivalent models without DAE to reduce verification complexity induced by DAE solver execution, and (b) a model simplification method, which automatically simplifies bond-graph models by replacing complex bond-graph components with simpler components for further verification overhead reductions. We successfully applied the proposed verification framework for safety verification of an automotive brake control system. The results of the study demonstrate that the automated model transformations of the CPS models yield significant verification complexity reductions without impairing the ability to detect unsafe behavior of the brake control system in a formal verification based on symbolic execution. © 2016 IEEE.

AB - The application of cyber-physical systems (CPSs) in safety-critical applications requires rigorous verification of their functional correctness and safety-relevant properties. We propose a practical verification framework which enables to fill the gaps between model-based development and the formal verification process seamlessly connecting them. The verification framework consists of (a) a model transformation method, which automatically transforms the plant models of CPSs including differential algebraic equations (DAE) to equivalent models without DAE to reduce verification complexity induced by DAE solver execution, and (b) a model simplification method, which automatically simplifies bond-graph models by replacing complex bond-graph components with simpler components for further verification overhead reductions. We successfully applied the proposed verification framework for safety verification of an automotive brake control system. The results of the study demonstrate that the automated model transformations of the CPS models yield significant verification complexity reductions without impairing the ability to detect unsafe behavior of the brake control system in a formal verification based on symbolic execution. © 2016 IEEE.

KW - bond-graph model

KW - cyber-physical systems

KW - Formal verification

KW - model transformation

KW - model-based development

KW - signal-flow model

KW - Algebra

KW - Automobile parts and equipment

KW - Brakes

KW - Control systems

KW - Cyber Physical System

KW - Differential equations

KW - Distributed computer systems

KW - Embedded systems

KW - Flow graphs

KW - Graph theory

KW - Reduction

KW - Safety engineering

KW - Signal flow graphs

KW - Ubiquitous computing

KW - Automated model transformations

KW - Bond graph model

KW - Cyber physical systems (CPSs)

KW - Differential algebraic equations

KW - Model based development

KW - Model transformation

KW - Model transformation methods

KW - Signal flow

U2 - 10.1109/CSE-EUC-DCABES.2016.154

DO - 10.1109/CSE-EUC-DCABES.2016.154

M3 - Conference contribution/Paper

SP - 1

EP - 8

BT - 2016 IEEE Intl Conference on Computational Science and Engineering (CSE) and IEEE Intl Conference on Embedded and Ubiquitous Computing (EUC) and 15th Intl Symposium on Distributed Computing and Applications for Business Engineering (DCABES)

PB - IEEE

ER -