 |
Conference papers
The Ten Lockheed Martin Cyber-Physical Challenges: Formalized, Analyzed, and Explained
Abstract : Capturing and analyzing requirements of Cyber-Physical Systems (CPS) can be challenging, since CPS models typically involve time-varying and real-valued variables, physical system dynamics, or even adaptive behavior. MATLAB/Simulink is a development and simulation framework that is widely used in industry to capture such systems. In this paper, we report on the application of NASA Ames tools to perform end-to-end analysis of the Ten Lockheed Martin Challenge Problems (LMCPS). LMCPS is a set of industrial Simulink model benchmarks and natural language requirements developed by domain experts. Our framework, which integrates the tools FRET and COCOSIM, is used to: 1) elicit, explain, and formalize the semantics of the given natural language requirements; 2) generate verification code and monitors that can be automatically attached to the Simulink models; 3) perform verification by using SMT-based model checkers. FRET and COCOS1M are open source, and can be used by other researchers and practitioners to replicate our case study. We provide a categorization of recurring patterns in the formalization of the requirements and discuss the strengths and weaknesses of our automated verification approach.
https://hal-enac.archives-ouvertes.fr/hal-02967437
Contributor : Laurence Porte <>
Submitted on : Tuesday, January 5, 2021 - 3:26:21 PM
Last modification on : Monday, January 18, 2021 - 1:49:44 PM
Long-term archiving on: : Wednesday, April 7, 2021 - 9:25:00 AM
Contributor : Laurence Porte <>
Submitted on : Tuesday, January 5, 2021 - 3:26:21 PM
Last modification on : Monday, January 18, 2021 - 1:49:44 PM
Long-term archiving on: : Wednesday, April 7, 2021 - 9:25:00 AM
File
main.pdf
Files produced by the author(s)