The Ten Lockheed Martin Cyber-Physical Challenges: Formalized, Analyzed, and Explained - Archive ouverte HAL Accéder directement au contenu
Communication Dans Un Congrès Année : 2021

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

(1) , (1) , (1) , (1) , (1) , (2) , (1)
1
2

Résumé

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.
Fichier principal
Vignette du fichier
main.pdf (484.13 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-02967437 , version 1 (05-01-2021)

Identifiants

Citer

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⟩
54 Consultations
152 Téléchargements

Altmetric

Partager

Gmail Facebook Twitter LinkedIn More