 |
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.
https://hal-enac.archives-ouvertes.fr/hal-02967437
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
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
Fichier
main.pdf
Fichiers produits par l'(les) auteur(s)