Home > Research > Publications & Outputs > Practical use of formal verification for safety...

Research

Associated organisational units

Links

Text available via DOI:

Keywords

View graph of relations

Practical use of formal verification for safety critical cyber-physical systems: A case study

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

Published

Standard

Practical use of formal verification for safety critical cyber-physical systems: A case study. / Ishigooka, T.; Saissi, H.; Piper, T. et al.
2014 IEEE International Conference on Cyber-Physical Systems, Networks, and Applications. IEEE, 2014. p. 7-12.

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 2014, Practical use of formal verification for safety critical cyber-physical systems: A case study. in 2014 IEEE International Conference on Cyber-Physical Systems, Networks, and Applications. IEEE, pp. 7-12. https://doi.org/10.1109/CPSNA.2014.20

APA

Ishigooka, T., Saissi, H., Piper, T., Winter, S., & Suri, N. (2014). Practical use of formal verification for safety critical cyber-physical systems: A case study. In 2014 IEEE International Conference on Cyber-Physical Systems, Networks, and Applications (pp. 7-12). IEEE. https://doi.org/10.1109/CPSNA.2014.20

Vancouver

Ishigooka T, Saissi H, Piper T, Winter S, Suri N. Practical use of formal verification for safety critical cyber-physical systems: A case study. In 2014 IEEE International Conference on Cyber-Physical Systems, Networks, and Applications. IEEE. 2014. p. 7-12 doi: 10.1109/CPSNA.2014.20

Author

Ishigooka, T. ; Saissi, H. ; Piper, T. et al. / Practical use of formal verification for safety critical cyber-physical systems : A case study. 2014 IEEE International Conference on Cyber-Physical Systems, Networks, and Applications. IEEE, 2014. pp. 7-12

Bibtex

@inproceedings{b07d627acdde4467ba09fbd1133cc4d7,
title = "Practical use of formal verification for safety critical cyber-physical systems: A case study",
abstract = "Cyber-Physical Systems (CPS) linking computing to physical systems are often used to monitor and controlsafety-critical processes, i.e. processes that bear the potential to cause significant damage or loss in the case of failures. While safety-critical systems have been extensively studied in both the discrete (computing) and analog (control) domains, the developed techniques apply to either one domain or the other. As cyber-physical systems span both domains, the focus on an individual domain leaves a gap on the systemlevel, where complex interactions between the domains can lead to failures that cannot be analyzed by considering only the physical orthe digital part of the integrated CPS. We discuss such a complex failure condition in a real-world brakecontrol system, and demonstrate its detection using a formalverification approach specifically targeting CPS. {\textcopyright} 2014 IEEE.",
keywords = "formal verification, safety critical cyber-physical systems, symbolic execution, Complex networks, Safety engineering, Security of data, Complex failure, Cyber physical systems (CPSs), Cyber-physical systems (CPS), Digital parts, Formal verifications, Physical systems, Safety critical systems, Symbolic execution, Embedded systems",
author = "T. Ishigooka and H. Saissi and T. Piper and S. Winter and Neeraj Suri",
note = "Cited By :4 ",
year = "2014",
month = aug,
day = "25",
doi = "10.1109/CPSNA.2014.20",
language = "English",
pages = "7--12",
booktitle = "2014 IEEE International Conference on Cyber-Physical Systems, Networks, and Applications",
publisher = "IEEE",

}

RIS

TY - GEN

T1 - Practical use of formal verification for safety critical cyber-physical systems

T2 - A case study

AU - Ishigooka, T.

AU - Saissi, H.

AU - Piper, T.

AU - Winter, S.

AU - Suri, Neeraj

N1 - Cited By :4

PY - 2014/8/25

Y1 - 2014/8/25

N2 - Cyber-Physical Systems (CPS) linking computing to physical systems are often used to monitor and controlsafety-critical processes, i.e. processes that bear the potential to cause significant damage or loss in the case of failures. While safety-critical systems have been extensively studied in both the discrete (computing) and analog (control) domains, the developed techniques apply to either one domain or the other. As cyber-physical systems span both domains, the focus on an individual domain leaves a gap on the systemlevel, where complex interactions between the domains can lead to failures that cannot be analyzed by considering only the physical orthe digital part of the integrated CPS. We discuss such a complex failure condition in a real-world brakecontrol system, and demonstrate its detection using a formalverification approach specifically targeting CPS. © 2014 IEEE.

AB - Cyber-Physical Systems (CPS) linking computing to physical systems are often used to monitor and controlsafety-critical processes, i.e. processes that bear the potential to cause significant damage or loss in the case of failures. While safety-critical systems have been extensively studied in both the discrete (computing) and analog (control) domains, the developed techniques apply to either one domain or the other. As cyber-physical systems span both domains, the focus on an individual domain leaves a gap on the systemlevel, where complex interactions between the domains can lead to failures that cannot be analyzed by considering only the physical orthe digital part of the integrated CPS. We discuss such a complex failure condition in a real-world brakecontrol system, and demonstrate its detection using a formalverification approach specifically targeting CPS. © 2014 IEEE.

KW - formal verification

KW - safety critical cyber-physical systems

KW - symbolic execution

KW - Complex networks

KW - Safety engineering

KW - Security of data

KW - Complex failure

KW - Cyber physical systems (CPSs)

KW - Cyber-physical systems (CPS)

KW - Digital parts

KW - Formal verifications

KW - Physical systems

KW - Safety critical systems

KW - Symbolic execution

KW - Embedded systems

U2 - 10.1109/CPSNA.2014.20

DO - 10.1109/CPSNA.2014.20

M3 - Conference contribution/Paper

SP - 7

EP - 12

BT - 2014 IEEE International Conference on Cyber-Physical Systems, Networks, and Applications

PB - IEEE

ER -