The Ten Lockheed Martin Cyber-Physical Challenges: Formalized, Analyzed, and Explained

Anastasia Mavridou (1) , Hamza Bourbouh (1) , Dimitra Giannakopoulou (1) , Thomas Pressburger (1) , Mohammad Hejase (1) , Pierre-Loïc Garoche (2) , Johann Schumann (1)

1 ARC - NASA Ames Research Center
2 ENAC - Ecole Nationale de l'Aviation Civile

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.

Domaines: Sciences de l'ingénieur [physics]

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⟩