Skip to Main content Skip to Navigation
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.
Document type :
Conference papers
Complete list of metadatas
Contributor : Laurence Porte <>
Submitted on : Wednesday, October 14, 2020 - 10:49:40 PM
Last modification on : Tuesday, October 20, 2020 - 10:32:07 AM




Anastasia Mavridou, Hamza Bourbouh, Dimitra Giannakopoulou, Thomas Pressburger, Mohammad Hejase, et al.. The Ten Lockheed Martin Cyber-Physical Challenges: Formalized, Analyzed, and Explained. IRE 2020 IEEE 28th International Requirements Engineering Conference, Aug 2020, Zurich, Switzerland. pp.300-310 / ISBN: 978-1-7281-7439-6, ⟨10.1109/RE48521.2020.00040⟩. ⟨hal-02967437⟩



Record views