Accéder directement au contenu Accéder directement à la navigation
Communication dans un congrès

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.
Type de document :
Communication dans un congrès
Liste complète des métadonnées
Contributeur : Laurence Porte Connectez-vous pour contacter le contributeur
Soumis le : mardi 5 janvier 2021 - 15:26:21
Dernière modification le : mardi 19 octobre 2021 - 11:02:55
Archivage à long terme le : : mercredi 7 avril 2021 - 09:25:00


Fichiers produits par l'(les) auteur(s)




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⟩



Consultations de la notice


Téléchargements de fichiers